L.not_mem_empty – Calculemus

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

PorJosé A. Alonso 24 agosto 202121 agosto 2021

Demostrar 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 Lean:

import tactic

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

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

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

example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
sorry

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

def particion (A : set (set X)) : Prop :=

(∀ x, (∃ B ∈ A, x ∈ B ∧ ∀ C ∈ A, x ∈ C → B = C)) ∧ ∅ ∉ A

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

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

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

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

lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz

-- 1ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        apply le_antisymm,
        { exact aux h hx, },
        { exact aux h (h.2.1 hx), }}}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

-- 2ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

-- 3ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use [clase R y,
         ⟨by use y,
          ⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

def particion (A : set (set X)) : Prop :=

(∀ x, (∃ B ∈ A, x ∈ B ∧ ∀ C ∈ A, x ∈ C → B = C)) ∧ ∅ ∉ A

lemma aux

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

λ z hz, h.2.2 hxy hz

-- 1ª demostración

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

begin

split,

{ simp,

intro y,

use (clase R y),

split,

{ use y, },

{ split,

{ exact h.1 y, },

{ intros x hx,

apply le_antisymm,

{ exact aux h hx, },

{ exact aux h (h.2.1 hx), }}}},

{ simp,

intros x hx,

have h1 : x ∈ clase R x := h.1 x,

rw ← hx at h1,

exact set.not_mem_empty x h1, },

end

-- 2ª demostración

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

begin

split,

{ simp,

intro y,

use (clase R y),

split,

{ use y, },

{ split,

{ exact h.1 y, },

{ intros x hx,

exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},

{ simp,

intros x hx,

have h1 : x ∈ clase R x := h.1 x,

rw ← hx at h1,

exact set.not_mem_empty x h1, },

end

-- 3ª demostración

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

begin

split,

{ simp,

intro y,

use [clase R y,

⟨by use y,

⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },

{ simp,

intros x hx,

have h1 : x ∈ clase R x := h.1 x,

rw ← hx at h1,

exact set.not_mem_empty x h1, },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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

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

ultimately show "∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C)"

by blast

qed

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

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]