El conjunto de las clases de equivalencia es una partición

José A. Alonso

03-07-2024

Demostrar con Lean4 que si \(R\) es una relación de equivalencia en \(X\), entonces las clases de equivalencia de \(R\) es una partición de \(X\).

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}

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

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

example
  (h : Equivalence R)
  : particion {a : Set X | ∃ s : X, a = clase R s} :=
by sorry

1. Demostración en lenguaje natural

Sea \(P = {[x] : x ∈ X}\). Tenemos que demostrar que \(P\) es una partición de \(X\); es decir, que \begin{align} &(∀x ∈ X)(∃B ∈ P)[x ∈ B ∧ (∀C ∈ P)[x ∈ C → B = C] \tag{1} \newline &∅ ∉ P \tag{2} \end{align}

Para demostrar (1) basta probar que \[ (∀x ∈ X)(∃y ∈ X)[x ∈ [y] ∧ (∀a ∈ X)[x ∈ [a] → [y] = [a]] \tag{3} \] Para ello sea \(x ∈ X\). Veamos que \([x]\) cumple las condiciones de (3); es decir, \[ x ∈ [x] ∧ (∀a ∈ X)[x ∈ [a] → [x] = [a]] \tag{4} \]

La primera condición de (4) se verifica puesto que \(R\) es reflexiva.

Para probar la segunda parte de (4), sea \(a ∈ X\) tal que \(x ∈ [a]\); es decir, \[ aRx \tag{5} \] y, puesto que \(R\) es simétrica, \[ xRa \tag{6} \] Entonces, \begin{align} z ∈ [x] &⟹ xRz \newline &⟹ aRz &&\text{[por (5) y la transitividad de \(R\)]} \newline &⟹ z ∈ [a] \newline z ∈ [a] &⟹ aRz \newline &⟹ xRz &&\text{[por (6) y la transitividad de \(R\)]} \newline &⟹ z ∈ [x] \end{align} Por tanto, \([x] = [a]\).

Para demostrar (2), supongamos que \(∅ ∈ P\). Entonces, existe un \(x ∈ X\) tal que \([x] = ∅\), lo cual es imposible porque \(x ∈ [x]\).

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}

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

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

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

example
  (h : Equivalence R)
  : particion {a : Set X | ∃ s : X, a = clase R s} :=
by
  set P := {a : Set X | ∃ s : X, a = clase R s}
  constructor
  . -- ⊢ (∀ x, ∃ B, B ∈ P) ∧ x ∈ B ∧ (∀ C, C ∈ P → x ∈ C → B = C)
    simp [P]
    -- ⊢ (∀ x, ∃ B, (∃ s, B = clase R s)) ∧ x ∈ B ∧ (∀ a, x ∈ clase R a → B = clase R a)
    intro x
    -- x : X
    -- ⊢ ∃ B, (∃ s, B = clase R s) ∧ x ∈ B ∧ (∀ a, x ∈ clase R a → B = clase R a)
    use (clase R x)
    -- ⊢ (∃ s, clase R x = clase R s) ∧ x ∈ clase R x ∧ (∀ a, y ∈ clase R a → clase R x = clase R a)
    constructor
    . -- ⊢ ∃ s, clase R x = clase R s
      use x
    . --   x ∈ clase R x ∧
      --   ∀ a, x ∈ clase R a → clase R x = clase R a
      constructor
      . -- ⊢ x ∈ clase R x
        exact h.1 x
      . -- ∀ a, x ∈ clase R a → clase R x = clase R a
        intros a ha
        -- a : X
        -- ha : x ∈ clase R a
        -- ⊢ clase R x = clase R a
        apply le_antisymm
        . -- ⊢ clase R x ≤ clase R a
          exact aux h ha
        . -- ⊢ clase R a ≤ clase R x
          exact aux h (h.2 ha)
  . -- ⊢ ¬∅ ∈ P
    simp [P]
    -- ⊢ ∀ (x : X), ¬∅ = clase R x
    intros x hx
    -- x : X
    -- hx : ∅ = clase R x
    -- ⊢ False
    have h1 : x ∈ clase R x := h.1 x
    rw [←hx] at h1
    -- h1 : x ∈ ∅
    exact Set.not_mem_empty x h1

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

example
  (h : Equivalence R)
  : particion {a : Set X | ∃ s : X, a = clase R s} :=
by
  set P := {a : Set X | ∃ s : X, a = clase R s}
  constructor
  . -- ⊢ (∀ x, ∃ B, B ∈ P) ∧ x ∈ B ∧ (∀ C, C ∈ P → x ∈ C → B = C)
    simp [P]
    -- ⊢ (∀ x, ∃ B, (∃ s, B = clase R s)) ∧ x ∈ B ∧ (∀ a, x ∈ clase R a → B = clase R a)
    intro x
    -- x : X
    -- ⊢ ∃ B, (∃ s, B = clase R s) ∧ x ∈ B ∧ (∀ a, x ∈ clase R a → B = clase R a)
    use (clase R x)
    -- ⊢ (∃ s, clase R x = clase R s) ∧ x ∈ clase R y ∧ (∀ a, x ∈ clase R a → clase R x = clase R a)
    repeat' constructor
    . -- ⊢ x ∈ clase R x
      exact h.1 x
    . -- ⊢ ∀ a, x ∈ clase R a → clase R x = clase R a
      intros a ha
      -- a : X
      -- ha : y ∈ clase R a
      -- ⊢ clase R a = clase R a
      exact le_antisymm (aux h ha) (aux h (h.2 ha))
  . -- ⊢ ¬∅ ∈ P
    simp [P]
    -- ⊢ ∀ (x : X), ¬∅ = clase R x
    intros x hx
    -- x : X
    -- hx : ∅ = clase R x
    -- ⊢ False
    have h1 : x ∈ clase R x := h.1 x
    rw [←hx] at h1
    -- h1 : x ∈ ∅
    exact Set.not_mem_empty x h1

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

-- variable (A B : Set X)
-- #check (Set.not_mem_empty x : x ∉ ∅)
-- #check (le_antisymm : A ≤ B → B ≤ A → A = B)

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

3. Demostraciones con Isabelle/HOL

theory El_conjunto_de_las_clases_de_equivalencia_es_una_particion
imports Main
begin

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

definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

lemma
  fixes   R :: "'a ⇒ 'a ⇒ bool"
  assumes "equivp R"
  shows   "particion (⋃x. {clase R x})" (is "particion ?P")
proof (unfold particion_def; intro conjI)
  show "(∀x. ∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C))"
  proof (intro allI)
    fix x
    have "clase R x ∈ ?P"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    moreover have "∀C∈?P. x ∈ C ⟶ clase R x = C"
    proof
      fix C
      assume "C ∈ ?P"
      then obtain y where "C = clase R y"
        by auto
      show "x ∈ C ⟶ clase R x = C"
      proof
        assume "x ∈ C"
        then have "R y x"
          using ‹C = clase R y› assms clase_def
          by (metis CollectD)
        then show "clase R x = C"
          using assms ‹C = clase R y› clase_def equivp_def
          by metis
      qed
    qed
    ultimately show "∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C)"
      by blast
  qed
next
  show "{} ∉ ?P"
  proof
    assume "{} ∈ ?P"
    then obtain x where "{} = clase R x"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    ultimately show False
      by simp
  qed
qed

end