Processing math: 100%
Skip to main content

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

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 (∀x∈X)(∃B∈P)[x∈B∧(∀C∈P)[x∈C→B=C]∅∉P

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

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 y, puesto que R es simétrica, xRa Entonces, z∈[x]⟹xRz⟹aRz[por (5) y la transitividad de R]⟹z∈[a]z∈[a]⟹aRz⟹xRz[por (6) y la transitividad de R]⟹z∈[x] 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