Si una función es creciente e involutiva, entonces es la identidad
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 involutiva si para todo x se tiene que f(f(x)) = x.
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
1. Demostración en lenguaje natural
Tenemos que demostrar que para todo x ∈ ℝ, f(x) = x. Sea x ∈ ℝ. Entonces, por ser f involutiva, se tiene que f(f(x)) = x \tag{1} Además, por las propiedades del orden, se tiene que f(x) ≤ x ó x ≤ f(x). Demostraremos que f(x) = x en los dos casos.
Caso 1: Supongamos que f(x) ≤ x \tag{2} Entonces, por ser f creciente, se tiene que f(f(x)) ≤ f(x) \tag{3} Sustituyendo (1) en (3), se tiene x ≤ f(x) que junto con (1) da f(x) = x
Caso 2: Supongamos que x ≤ f(x) \tag{4} Entonces, por ser f creciente, se tiene que f(x) ≤ f(f(x)) \tag{5} Sustituyendo (1) en (5), se tiene f(x) ≤ x que junto con (4) da f(x) = x
2. Demostraciones con Lean4
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) -- 1ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by funext x -- x : ℝ -- ⊢ f x = id x have h : f (f x) = x := hi x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x have h1a : f (f x) ≤ f x := hc h1 have h1b : x ≤ f x := by rwa [h] at h1a show f x = x exact antisymm h1 h1b . -- h2 : x ≤ f x have h2a : f x ≤ f (f x) := hc h2 have h2b : f x ≤ x := by rwa [h] at h2a show f x = x exact antisymm h2b h2 -- 2ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by unfold Monotone Involutive at * -- hc : ∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b -- hi : ∀ (x : ℝ), f (f x) = x funext x -- x : ℝ -- ⊢ f x = id x unfold id -- ⊢ f x = x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x apply antisymm h1 -- ⊢ x ≤ f x have h3 : f (f x) ≤ f x := by apply hc -- ⊢ f x ≤ x exact h1 rwa [hi] at h3 . -- h2 : x ≤ f x apply antisymm _ h2 -- ⊢ f x ≤ x have h4 : f x ≤ f (f x) := by apply hc -- ⊢ x ≤ f x exact h2 rwa [hi] at h4 -- 3ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by funext x -- x : ℝ -- ⊢ f x = id x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x apply antisymm h1 -- ⊢ x ≤ f x have h3 : f (f x) ≤ f x := hc h1 rwa [hi] at h3 . -- h2 : x ≤ f x apply antisymm _ h2 -- ⊢ f x ≤ x have h4 : f x ≤ f (f x) := hc h2 rwa [hi] at h4 -- 4ª demostración example (hc : Monotone f) (hi : Involutive f) : f = id := by funext x -- x : ℝ -- ⊢ f x = id x cases' (le_total (f x) x) with h1 h2 . -- h1 : f x ≤ x apply antisymm h1 -- ⊢ x ≤ f x calc x = f (f x) := (hi x).symm _ ≤ f x := hc h1 . -- h2 : x ≤ f x apply antisymm _ h2 -- ⊢ f x ≤ x calc f x ≤ f (f x) := hc h2 _ = x := hi x -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (le_total a b : a ≤ b ∨ b ≤ a) -- #check (antisymm : a ≤ b → b ≤ a → a = b)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
theory Una_funcion_creciente_e_involutiva_es_la_identidad imports Main HOL.Real begin definition involutiva :: "(real ⇒ real) ⇒ bool" where "involutiva f ⟷ (∀x. f (f x) = x)" (* 1ª demostración *) lemma fixes f :: "real ⇒ real" assumes "mono f" "involutiva f" shows "f = id" proof (unfold fun_eq_iff; intro allI) fix x have "x ≤ f x ∨ f x ≤ x" by (rule linear) then have "f x = x" proof (rule disjE) assume "x ≤ f x" then have "f x ≤ f (f x)" using assms(1) by (simp only: monoD) also have "… = x" using assms(2) by (simp only: involutiva_def) finally have "f x ≤ x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by (simp only: antisym) next assume "f x ≤ x" have "x = f (f x)" using assms(2) by (simp only: involutiva_def) also have "... ≤ f x" using ‹f x ≤ x› assms(1) by (simp only: monoD) finally have "x ≤ f x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by (simp only: monoD) qed then show "f x = id x" by (simp only: id_apply) qed (* 2ª demostración *) lemma fixes f :: "real ⇒ real" assumes "mono f" "involutiva f" shows "f = id" proof fix x have "x ≤ f x ∨ f x ≤ x" by (rule linear) then have "f x = x" proof assume "x ≤ f x" then have "f x ≤ f (f x)" using assms(1) by (simp only: monoD) also have "… = x" using assms(2) by (simp only: involutiva_def) finally have "f x ≤ x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by auto next assume "f x ≤ x" have "x = f (f x)" using assms(2) by (simp only: involutiva_def) also have "... ≤ f x" by (simp add: ‹f x ≤ x› assms(1) monoD) finally have "x ≤ f x" by this show "f x = x" using ‹f x ≤ x› ‹x ≤ f x› by auto qed then show "f x = id x" by simp qed (* 3ª demostración *) lemma fixes f :: "real ⇒ real" assumes "mono f" "involutiva f" shows "f = id" proof fix x have "x ≤ f x ∨ f x ≤ x" by (rule linear) then have "f x = x" proof assume "x ≤ f x" then have "f x ≤ x" by (metis assms involutiva_def mono_def) then show "f x = x" using ‹x ≤ f x› by auto next assume "f x ≤ x" then have "x ≤ f x" by (metis assms involutiva_def mono_def) then show "f x = x" using ‹f x ≤ x› by auto qed then show "f x = id x" by simp qed end