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

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)

100

101

102

103

104

105

106

107

108

109

import Mathlib.Data.Real.Basic

open Function

variable (f : ℝ → ℝ)

-- 1ª demostración

example

(hc : Monotone f)

(hi : Involutive f)

: f = id :=

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 :=

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 :=

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 :=

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

100

101

102

103

104

105

106

107

108

109

110

111

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)

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

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

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

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply