Skip to main content

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…

Si g ∘ f es suprayectiva, entonces g es suprayectiva

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

Read more…

Si g ∘ f es inyectiva, entonces f es inyectiva

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

Read more…

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

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

Read more…

Las funciones con inversa por la izquierda son inyectivas

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

Read more…

La congruencia módulo 2 es una relación de equivalencia

Relación de equivalencia

Se define la relación \(R\) entre los números enteros de forma que \(x\) está relacionado con \(y\) si \(x-y\) es divisible por 2.

Demostrar con Lean4 que \(R\) es una relación de equivalencia.

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

import Mathlib.Tactic

def R (m n : ℤ) := 2 ∣ (m - n)

example : Equivalence R :=
by sorry

Read more…

Si uₙ está acotada y el límite de vₙ es 0, entonces el límite de uₙ·vₙ es 0

Límites

Demostrar con Lean4 que si \(u_n\) está acotada y el límite de \(v_n\) es \(0\), entonces el límite de \(u_n·v_n\) es \(0\).

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

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

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

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

def acotada (a : ℕ → ℝ) :=
  ∃ B, ∀ n, |a n| ≤ B

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
by sorry

Read more…

Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ

Límites

En Lean4, una sucesión \(u_0, u_1, u_2, \dots\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el \(n\)-ésimo término de la sucesión.

Se define que \(a\) límite de la sucesión \(u\) como sigue

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

Demostrar que si \((∀ n)[u_n ≤ v_n]\), \(a\) es límite de \(u_n\) y \(c\) es límite de \(v_n\), entonces \(a ≤ c\).

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 (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by sorry

Read more…