Skip to main content

La equipotencia es una relación transitiva

Funciones

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar con Lean4 que la relación de equipotencia es transitiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

def es_equipotente (A B : Type _) :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

example : Transitive (. ⋍ .) :=
by sorry

Read more…

La composición de funciones biyectivas es biyectiva

Funciones

Demostrar con Lean4 que la composición de dos funciones biyectivas es una función biyectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {X Y Z : Type}
variable {f : X → Y}
variable {g : Y → Z}

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by sorry

Read more…

La equipotencia es una relación simétrica

Funciones

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar con Lean4 que la relación de equipotencia es simétrica.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

lemma aux1
  (hf : Bijective f)
  : tiene_inversa f :=
by
  cases' (bijective_iff_has_inverse.mp hf) with g hg
  -- g : Y → X
  -- hg : LeftInverse g f ∧ Function.RightInverse g f
  aesop (add norm unfold [tiene_inversa, inversa])

lemma aux2
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

example : Symmetric (. ⋍ .) :=
by sorry

Read more…

La inversa de una función es biyectiva

Funciones

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

Demostrar con Lean4 que si \(g\) es una inversa de \(f\), entonces \(g\) es biyectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)
variable (g : Y → X)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

example
  (hg : inversa g f)
  : Bijective g :=
by sorry

Read more…

La equipotencia es una relación reflexiva

Funciones

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar que la relación de equipotencia es reflexiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

example : Reflexive (. ⋍ .) :=
by sorry

Read more…

Las funciones biyectivas tienen inversa

Funciones

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

y que \(f\) tiene inversa por

   def tiene_inversa (f : X → Y) :=
     ∃ g, inversa f g

Demostrar con Lean4 que si la función \(f\) es biyectiva, entonces \(f\) tiene inversa.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

example
  (hf : Bijective f)
  : tiene_inversa f :=
by sorry

Read more…

Las funciones con inversa son biyectivas

Funciones

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

y que \(f\) tiene inversa por

   def tiene_inversa (f : X → Y) :=
     ∃ g, inversa g f

Demostrar con Lean4 que si la función \(f\) tiene inversa, entonces \(f\) es biyectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

example
  (hf : tiene_inversa f)
  : Bijective f :=
by sorry

Read more…

Las funciones suprayectivas tienen inversa por la derecha

Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

que \(g\) es una inversa por la derecha de \(f\) está definido por

   RightInverse (g : β → α) (f : α → β) : Prop :=
      LeftInverse f g

y que \(f\) tenga inversa por la derecha está definido por

   HasRightInverse (f : α → β) : Prop :=
      ∃ g : β → α, RightInverse g f

Finalmente, que \(f\) es suprayectiva está definido por

   def Surjective (f : α → β) : Prop :=
      ∀ b, ∃ a, f a = b

Demostrar con Lean4 que si \(f\) es una función suprayectiva, entonces \(f\) tiene inversa por la derecha.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function Classical

variable {α β: Type _}
variable {f : α → β}

example
  (hf : Surjective f)
  : HasRightInverse f :=
by sorry

Read more…

Las funciones con inversa por la derecha son suprayectivas

Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

que \(g\) es una inversa por la derecha de \(f\) está definido por

   RightInverse (g : β → α) (f : α → β) : Prop :=
      LeftInverse f g

y que \(f\) tenga inversa por la derecha está definido por

   HasRightInverse (f : α → β) : Prop :=
      ∃ g : β → α, RightInverse g f

Finalmente, que \(f\) es suprayectiva está definido por

   def Surjective (f : α → β) : Prop :=
      ∀ b, ∃ a, f a = b

Demostrar con Lean4 que si la función \(f\) tiene inversa por la derecha, entonces \(f\) es suprayectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {α β: Type _}
variable {f : α → β}

example
  (hf : HasRightInverse f)
  : Surjective f :=
by sorry

Read more…

Las funciones inyectivas tienen inversa por la izquierda

Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

y que \(f\) tenga inversa por la izquierda está definido por

   HasLeftInverse (f : α → β) : Prop :=
      ∃ finv : β → α, LeftInverse finv f

Finalmente, que \(f\) es inyectiva está definido por

   Injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

Demostrar con Lean4 que si \(f\) es una función inyectiva con dominio no vacío, entonces \(f\) tiene inversa por la izquierda.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

open Function Classical

variable {α β: Type _}
variable {f : α → β}

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by sorry

Read more…