Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que \[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \] entonces \(f\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by sorry
Sea una función \(f\) de \(ℝ\) en \(ℝ\).
En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f
Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (hc : Monotone f) (hi : Involutive f) : f = id := by sorry
Sea una función \(f\) de \(ℝ\) en \(ℝ\). Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\). Se dice que \(f\) es decreciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≥ f(y)\).
Demostrar con Lean4 que si \(f\) es creciente y \(g\) es decreciente, entonces \(g ∘ f\) es decreciente.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) def creciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≤ f y def decreciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≥ f y example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by sorry
Demostrar con Lean4 que la función \(x ↦ -x\) no es monótona creciente.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic example : ¬Monotone fun x : ℝ ↦ -x := by sorry
Demostrar con Lean4 que \(f: ℝ → ℝ\) no es monótona syss \((∃x,y)[x ≤ y ∧ f(x) > f(y)]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} example : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := sorry
Demostrar con Lean4 que si \(f\) no es monótona, entonces ()∃x∃y[x ≤ y ∧ f(y) < f(x)]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable (f : ℝ → ℝ) example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by sorry
Demostrar con Lean4 que si \(¬(∀a)(∃x)[f(x) > a]\), entonces \(f\) está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by sorry
Demostrar con Lean4 que si \(f\) no está acotada superiormente, entonces \((∀a)(∃x)[f(x) > a]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬acotadaSup f) : ∀ a, ∃ x, f x > a := by sorry
Demostrar con Lean4 que no para toda \(f : ℝ → ℝ\) monótona, \((∀a,b)[f(a) ≤ f(b) → a ≤ b]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by sorry
Demostrar con Lean4 que si \(a, b ∈ ℝ\) tales que \(a ≤ b\) y \(f(b) < f(a)\), entonces \(f\) no es monótona
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by sorry