La equipotencia es una relación reflexiva

José A. Alonso

18-06-2024

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

Las funciones biyectivas tienen inversa

José A. Alonso

17-06-2024

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

Las funciones con inversa son biyectivas

José A. Alonso

14-06-2024

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

Las funciones suprayectivas tienen inversa por la derecha

José A. Alonso

13-06-2024

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

Las funciones con inversa por la derecha son suprayectivas

José A. Alonso

12-06-2024

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

Las funciones inyectivas tienen inversa por la izquierda

José A. Alonso

11-06-2024

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

Si g ∘ f es suprayectiva, entonces g es suprayectiva

José A. Alonso

10-06-2024

Funciones

Sean \(f: X → Y\) y \(g: Y → Z\). Demostrar que si \(g ∘ f\) es suprayectiva, entonces \(g\) es suprayectiva.

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
  (h : Surjective (g ∘ f))
  : Surjective g :=
by sorry

Si g ∘ f es inyectiva, entonces f es inyectiva

José A. Alonso

07-06-2024

Funciones

Sean \(f: X → Y\) y \(g: Y → Z\). Demostrar con Lean4 que si \(g ∘ f\) es inyectiva, entonces \(f\) es inyectiva.

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
  (h : Injective (g ∘ f))
  : Injective f :=
by sorry

Si el límite de la sucesión uₙ es a, entonces el límite de -uₙ es -a

José A. Alonso

06-06-2024

Límites

En Lean4, una sucesión \(u₀, u₁, u₂, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(uₙ\).

Se define que \(c\) es el límite de la sucesión \(u\), por

   def limite : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

Demostrar con Lean4 que que si el límite de \(u_n\) es \(a\), entonces el de \(-u_n\) es \(-a\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (u v : ℕ → ℝ)
variable (a c : ℝ)

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : limite u a)
  : limite (fun n ↦ -u n) (-a) :=
by sorry

Las funciones con inversa por la izquierda son inyectivas

José A. Alonso

05-06-2024

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\) tiene inversa por la izquierda, entonces \(f\) es inyectiva.

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

import Mathlib.Tactic
open Function

universe u v
variable {α : Type u}
variable {β : Type v}
variable {f : α → β}

example
  (hf : HasLeftInverse f)
  : Injective f :=
by sorry