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
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
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
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
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
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
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
Demostrar con Lean4 que si \(x, y ∈ ℝ\) tales que \((∀ z)[y < z → x ≤ z]\), entonces \(x ≤ y\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by sorry
Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (Hombre : Type) variable (afeita : Hombre → Hombre → Prop) example : ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) := by sorry
Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir, \[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε -- (convergente u) expresa que u es convergente. def convergente (u : ℕ → ℝ) := ∃ a, limite u a example (h : convergente u) : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b := by sorry