Demostrar con Lean4 que la función identidad no está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
import src.Funcion_no_acotada_superiormente example : ¬ acotadaSup (fun x ↦ x) := by sorry
Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) < a\), entonces \(f\) no tiene cota inferior.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def acotadaInf (f : ℝ → ℝ) : Prop := ∃ a, CotaInferior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by sorry
Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) : Prop := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by sorry
Demostrar con Lean4 que en \(ℝ\), \(a < b → ¬(b < a)\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (a b : ℝ) example (h : a < b) : ¬ b < a := by sorry
Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by sorry
Demostrar con Lean4 que si \(f: ℝ → ℝ\) es suprayectiva, entonces \(∃x ∈ ℝ\) tal que \(f(x)² = 9\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic open Function example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, (f x)^2 = 9 := by sorry
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx + d\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {c d : ℝ} open Function example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by sorry
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by sorry
Demostrar con Lean4 que la función \(x ↦ x + c\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {c : ℝ} open Function example : Surjective (fun x ↦ x + c) := by sorry
Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {a b c : ℕ} example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by sorry