Demostrar con Lean4 que si \(f\) es monótona y \(f(a) < f(b)\), entonces \(a < b\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : Monotone f) (h2 : f a < f b) : a < b := by sorry
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 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 \(c ≥ 0\) y \(f\) está acotada superiormente, entonces \(c·f\) también lo está.
Para ello, completar la siguiente teoría de Lean4:
import src.Cota_superior_de_producto_por_escalar variable {f : ℝ → ℝ} variable {c : ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a example (hf : acotadaSup f) (hc : c ≥ 0) : acotadaSup (fun x ↦ c * f x) := by sorry