Las_clases_de_equivalencia_de_elementos_relacionados_son_iguales.md

title	date	category	has_math
Las clases de equivalencia de elementos relacionados son iguales	2024-07-01 06:00:00 UTC+02:00	Relaciones de equivalencia	true

[mathjax]

Demostrar con Lean4 que las clases de equivalencia de elementos relacionados son iguales.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

variable {X : Type}
variable {x y: X}
variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
by sorry

1. Demostración en lenguaje natural

Sean \(x, y ∈ X\) tales que \[ xRy \tag{1} \] Tenemos que demostrar que \([x] = [y]\); es decir, que \begin{align} &[y] ⊆ [x] \tag{2} \\ &[x] ⊆ [y] \tag{3} \end{align}

Para demostrar (2), sea \(z ∈ [y]\). Entonces, \[ yRz \] entonces, por (1) y por ser \(R\) transitiva, \[ xRz \] Luego, \(z ∈ [x]\).

Para demostrar (2), se observa que por (1) y por ser \(R\) simétrica, se tiene que \(yRx\) y se puede usar el mismo razonamiento del caso anterior.

2. Demostraciones con Lean4

import Mathlib.Tactic

variable {X : Type}
variable {x y: X}
variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

-- En la demostración se usará el siguiente lema del que se presentan
-- varias demostraciones.

-- 1ª demostración del lema auxiliar
-- =================================

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
by
  intros z hz
  -- z : X
  -- hz : z ∈ clase R y
  -- ⊢ z ∈ clase R x
  have hyz : R y z := hz
  have htrans : Transitive R := Equivalence.transitive h
  have hxz : R x z := htrans hxy hyz
  exact hxz

-- 2ª demostración del lema auxiliar
-- =================================

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
by
  intros z hz
  -- z : X
  -- hz : z ∈ clase R y
  -- ⊢ z ∈ clase R x
  exact (Equivalence.transitive h) hxy hz

-- 3ª demostración del lema auxiliar
-- =================================

lemma aux
  (h : Equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
fun _ hz ↦ (Equivalence.transitive h) hxy hz

-- A continuación se presentan varias demostraciones del ejercicio
-- usando el lema auxiliar

-- 1ª demostración
-- ===============

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
by
  apply le_antisymm
  . -- ⊢ clase R x ≤ clase R y
    have hs : Symmetric R := Equivalence.symmetric h
    have hyx : R y x := hs hxy
    exact aux h hyx
  . -- ⊢ clase R y ≤ clase R x
    exact aux h hxy

-- 2ª demostración
-- ===============

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
by
  apply le_antisymm
  . -- ⊢ clase R x ≤ clase R y
    exact aux h (Equivalence.symmetric h hxy)
  . -- ⊢ clase R y ≤ clase R x
    exact aux h hxy

-- 3ª demostración
-- ===============

example
  (h : Equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
le_antisymm (aux h (Equivalence.symmetric h hxy)) (aux h hxy)

-- Lemas usados
-- ============

-- variable (x y z : Set X)
-- #check (Equivalence.symmetric : Equivalence R → Symmetric R)
-- #check (Equivalence.transitive : Equivalence R → Transitive R)
-- #check (le_antisymm : x ≤ y → y ≤ x → x = y)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory Las_clases_de_equivalencia_de_elementos_relacionados_son_iguales
imports Main
begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"
  where "clase R x = {y. R x y}"

(* En la demostración se usará el siguiente lema del que se presentan
   varias demostraciones. *)

(* 1ª demostración del lema auxiliar *)

lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y ⊆ clase R x"
proof (rule subsetI)
  fix z
  assume "z ∈ clase R y"
  then have "R y z"
    by (simp add: clase_def)
  have "transp R"
    using assms(1) by (rule equivp_imp_transp)
  then have "R x z"
    using ‹R x y› ‹R y z› by (rule transpD)
  then show "z ∈ clase R x"
    by (simp add: clase_def)
qed

(* 2ª demostración del lema auxiliar *)

lemma aux :
  assumes "equivp R"
          "R x y"
  shows "clase R y ⊆ clase R x"
  using assms
  by (metis clase_def eq_refl equivp_def)

(* A continuación se presentan demostraciones del ejercicio *)

(* 1ª demostración *)

lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y = clase R x"
proof (rule equalityI)
  show "clase R y ⊆ clase R x"
    using assms by (rule aux)
next
  show "clase R x ⊆ clase R y"
  proof -
    have "symp R"
      using assms(1) equivpE by blast
    have "R y x"
      using ‹R x y› by (simp add: ‹symp R› sympD)
    with assms(1) show "clase R x ⊆ clase R y"
       by (rule aux)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y = clase R x"
  using assms
  by (metis clase_def equivp_def)

end