Relaciones – Página 2

Las clases de equivalencia contienen a las clases de equivalencia de sus elementos

PorJosé A. Alonso 3 octubre 20212 octubre 2021

Este ejercicio es el 4º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.

El ejercicio consiste en demostrar que si C es una clase de equivalencia y a ∈ C, entonces la clase de equivalencia de a está contenida en C.

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

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

example
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
sorry

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

example

{hR: equivalence R}

{a b : A}

: a ∈ clase R b → clase R a ⊆ clase R b :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

-- Se usará el siguiente lema auxiliar
lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

-- 1ª demostración
example
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
begin
  intro hab,
  intros z hza,
  rw pertenece_clase_syss at hab hza ⊢,
  obtain ⟨-, -, htrans⟩ := hR,
  exact htrans hza hab,
end

-- 2ª demostración
example
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
begin
  intros hab z hza,
  exact hR.2.2 hza hab,
end

-- 3ª demostración
lemma subclase_si_pertenece
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
λ hab z hza, hR.2.2 hza hab

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

-- Se usará el siguiente lema auxiliar

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

-- 1ª demostración

example

{hR: equivalence R}

{a b : A}

: a ∈ clase R b → clase R a ⊆ clase R b :=

begin

intro hab,

intros z hza,

rw pertenece_clase_syss at hab hza ⊢,

obtain ⟨-, -, htrans⟩ := hR,

exact htrans hza hab,

end

-- 2ª demostración

example

{hR: equivalence R}

{a b : A}

: a ∈ clase R b → clase R a ⊆ clase R b :=

begin

intros hab z hza,

exact hR.2.2 hza hab,

end

-- 3ª demostración

lemma subclase_si_pertenece

{hR: equivalence R}

{a b : A}

: a ∈ clase R b → clase R a ⊆ clase R b :=

λ hab z hza, hR.2.2 hza hab

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]

Pertenencia a su propia clase de equivalencia

PorJosé A. Alonso 2 octubre 20212 octubre 2021

Este ejercicio es el 3º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.

En este empezamos con las relaciones de equivalencia, que están definidas en Lean por:

   reflexive R := ∀ (x : A), R x x
   symmetric R := ∀ ⦃x y : A⦄, R x y → R y x
   transitive R := ∀ ⦃x y z : A⦄, R x y → R y z → R x z
   equivalence R := reflexive R ∧ symmetric R ∧ transitive R

reflexive R := ∀ (x : A), R x x

symmetric R := ∀ ⦃x y : A⦄, R x y → R y x

transitive R := ∀ ⦃x y z : A⦄, R x y → R y z → R x z

equivalence R := reflexive R ∧ symmetric R ∧ transitive R

donde A un tipo y R: A → A → Prop es una relación binaria en A.

Además, en Lean se puede definir la clase de equivalencia de un elemento a respecto de una relación de equivalencia R por

   def clase (a : A) :=
     {b : A | R b a}

1 2	def clase (a : A) := {b : A \| R b a}

Demostrar que cada elemento pertenece a su clase de equivalencia.

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

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

example
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
sorry

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

example

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

-- Se usará el siguiente lema auxiliar
lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

-- 1ª demostración
example
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
begin
  rw pertenece_clase_syss,
  suffices h : reflexive R,
  { exact h a, },
  { rcases hR with ⟨h2, -, -⟩,
    exact h2, },
end

-- 1ª demostración
example
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
begin
  rw pertenece_clase_syss,
  suffices h : reflexive R,
  { exact h a, },
  { exact hR.1, },
end

-- 3ª demostración
example
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
begin
  rw pertenece_clase_syss,
  rcases hR with ⟨hrefl, -, -⟩,
  exact hrefl a,
end

-- 4ª demostración
example
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
begin
  obtain ⟨hrefl, -, -⟩ := hR,
  rw pertenece_clase_syss,
  apply hrefl,
end

-- 5ª demostración
example
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
begin
  rw pertenece_clase_syss,
  apply hR.1,
end

-- 6ª demostración
lemma pertenece_clase_propia
  {hR : equivalence R}
  (a : A)
  : a ∈ clase R a :=
(pertenece_clase_syss R).mpr (hR.1 a)

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

-- Se usará el siguiente lema auxiliar

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

-- 1ª demostración

example

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

begin

rw pertenece_clase_syss,

suffices h : reflexive R,

{ exact h a, },

{ rcases hR with ⟨h2, -, -⟩,

exact h2, },

end

-- 1ª demostración

example

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

begin

rw pertenece_clase_syss,

suffices h : reflexive R,

{ exact h a, },

{ exact hR.1, },

end

-- 3ª demostración

example

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

begin

rw pertenece_clase_syss,

rcases hR with ⟨hrefl, -, -⟩,

exact hrefl a,

end

-- 4ª demostración

example

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

begin

obtain ⟨hrefl, -, -⟩ := hR,

rw pertenece_clase_syss,

apply hrefl,

end

-- 5ª demostración

example

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

begin

rw pertenece_clase_syss,

apply hR.1,

end

-- 6ª demostración

lemma pertenece_clase_propia

{hR : equivalence R}

(a : A)

: a ∈ clase R a :=

(pertenece_clase_syss R).mpr (hR.1 a)

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]

Las particiones definen relaciones de equivalencia

PorJosé A. Alonso 28 agosto 202123 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada elemento de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

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

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

Demostrar que si P es una partición de X, entonces la relación definida por P es una relación de equivalencia.

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

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

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

example
  (h : particion P)
  : equivalence (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

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

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

example

(h : particion P)

: equivalence (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

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

example
  (h : particion P)
  : equivalence (relacion P) :=
begin
  repeat { split },
  { intro x,
    rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,
    use [A, ⟨hAP, hxA, hxA⟩], },
  { intros x y hxy,
    rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
    use [B, ⟨hBP, hyB, hxB⟩], },
  { rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
    use B1,
    repeat { split },
    { exact hB1P, },
    { exact hxB1, },
    { convert hzB2,
      rcases (h.1 y) with ⟨B, -, -, hB⟩,
      exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), }},
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

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

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

example

(h : particion P)

: equivalence (relacion P) :=

begin

repeat { split },

{ intro x,

rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,

use [A, ⟨hAP, hxA, hxA⟩], },

{ intros x y hxy,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use [B, ⟨hBP, hyB, hxB⟩], },

{ rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,

use B1,

repeat { split },

{ exact hB1P, },

{ exact hxB1, },

{ convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), }},

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 Las_particiones_definen_relaciones_de_equivalencia
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

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

(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "equivp (relacion P)"
proof (rule equivpI)
  show "reflp (relacion P)"
  proof (rule reflpI)
    fix x
    obtain A where "A ∈ P ∧ x ∈ A"
      using assms particion_def by metis
    then show "relacion P x x"
      using relacion_def by metis
  qed
next
  show "symp (relacion P)"
  proof (rule sympI)
    fix x y
    assume "relacion P x y"
    then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"
      using relacion_def by metis
    then show "relacion P y x"
      using relacion_def by metis
  qed
next
  show "transp (relacion P)"
  proof (rule transpI)
    fix x y z
    assume "relacion P x y" and "relacion P y z"
    obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
      using ‹relacion P x y› by (meson relacion_def)
    obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
      using ‹relacion P y z› by (meson relacion_def)
    have "A = B"
    proof -
      obtain C where "C ∈ P"
                 and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
        using assms particion_def by metis
      then show "A = B"
        using ‹A ∈ P› ‹B ∈ P› hA hB by blast
    qed
    then have "x ∈ A ∧ z ∈ A"  using hA hB by auto
    then show "relacion P x z"
      using ‹A = B› ‹A ∈ P› relacion_def by metis
  qed
qed

(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "equivp (relacion P)"
proof (rule equivpI)
  show "reflp (relacion P)"
    using assms particion_def relacion_def
    by (metis reflpI)
next
  show "symp (relacion P)"
    using assms relacion_def
    by (metis sympI)
next
  show "transp (relacion P)"
    using assms relacion_def particion_def
    by (smt (verit) transpI)
qed

end

theory Las_particiones_definen_relaciones_de_equivalencia

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where

"particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)

lemma

assumes "particion P"

shows "equivp (relacion P)"

proof (rule equivpI)

show "reflp (relacion P)"

proof (rule reflpI)

fix x

obtain A where "A ∈ P ∧ x ∈ A"

using assms particion_def by metis

then show "relacion P x x"

using relacion_def by metis

qed

show "symp (relacion P)"

proof (rule sympI)

fix x y

assume "relacion P x y"

then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"

using relacion_def by metis

then show "relacion P y x"

using relacion_def by metis

qed

show "transp (relacion P)"

proof (rule transpI)

fix x y z

assume "relacion P x y" and "relacion P y z"

obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"

using ‹relacion P x y› by (meson relacion_def)

obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"

using ‹relacion P y z› by (meson relacion_def)

have "A = B"

proof -

obtain C where "C ∈ P"

and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

using assms particion_def by metis

then show "A = B"

using ‹A ∈ P› ‹B ∈ P› hA hB by blast

qed

then have "x ∈ A ∧ z ∈ A" using hA hB by auto

then show "relacion P x z"

using ‹A = B› ‹A ∈ P› relacion_def by metis

qed

(* 2ª demostración *)

lemma

assumes "particion P"

shows "equivp (relacion P)"

proof (rule equivpI)

show "reflp (relacion P)"

using assms particion_def relacion_def

by (metis reflpI)

show "symp (relacion P)"

using assms relacion_def

by (metis sympI)

show "transp (relacion P)"

using assms relacion_def particion_def

by (smt (verit) transpI)

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]

Las particiones definen relaciones transitivas

PorJosé A. Alonso 27 agosto 202121 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

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

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

Demostrar que si P es una partición de X, entonces la relación definida por P es transitiva.

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

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

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

example
  (h : particion P)
  : transitive (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

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

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

example

(h : particion P)

: transitive (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

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

-- 1ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  unfold transitive,
  intros x y z h1 h2,
  unfold relacion at *,
  rcases h1 with ⟨B1, hB1P, hxB1, hyB1⟩,
  rcases h2 with ⟨B2, hB2P, hyB2, hzB2⟩,
  use B1,
  repeat { split },
  { exact hB1P, },
  { exact hxB1, },
  { convert hzB2,
    rcases (h.1 y) with ⟨B, -, -, hB⟩,
    have hBB1 : B = B1 := hB B1 hB1P hyB1,
    have hBB2 : B = B2 := hB B2 hB2P hyB2,
    exact eq.trans hBB1.symm hBB2, },
end

-- 2ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
  use B1,
  repeat { split },
  { exact hB1P, },
  { exact hxB1, },
  { convert hzB2,
    rcases (h.1 y) with ⟨B, -, -, hB⟩,
    exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), },
end

-- 3ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
  use [B1, ⟨hB1P,
            hxB1,
            by { convert hzB2,
                 rcases (h.1 y) with ⟨B, -, -, hB⟩,
                 exact eq.trans (hB B1 hB1P hyB1).symm
                                (hB B2 hB2P hyB2), }⟩],
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

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

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

-- 1ª demostración

example

(h : particion P)

: transitive (relacion P) :=

begin

unfold transitive,

intros x y z h1 h2,

unfold relacion at *,

rcases h1 with ⟨B1, hB1P, hxB1, hyB1⟩,

rcases h2 with ⟨B2, hB2P, hyB2, hzB2⟩,

use B1,

repeat { split },

{ exact hB1P, },

{ exact hxB1, },

{ convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

have hBB1 : B = B1 := hB B1 hB1P hyB1,

have hBB2 : B = B2 := hB B2 hB2P hyB2,

exact eq.trans hBB1.symm hBB2, },

end

-- 2ª demostración

example

(h : particion P)

: transitive (relacion P) :=

begin

rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,

use B1,

repeat { split },

{ exact hB1P, },

{ exact hxB1, },

{ convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), },

end

-- 3ª demostración

example

(h : particion P)

: transitive (relacion P) :=

begin

rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,

use [B1, ⟨hB1P,

hxB1,

by { convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

exact eq.trans (hB B1 hB1P hyB1).symm

(hB B2 hB2P hyB2), }⟩],

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 Las_particiones_definen_relaciones_transitivas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

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

(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  have "∃A∈P. x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (simp only: relacion_def)
  then obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    by (rule bexE)
  have "∃B∈P. y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (simp only: relacion_def)
  then obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    by (rule bexE)
  have "A = B"
  proof -
    have "∃C ∈ P. y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms
      by (simp only: particion_def)
    then obtain C where "C ∈ P"
                    and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      by (rule bexE)
    have hC' : "∀D∈P. y ∈ D ⟶ C = D"
      using hC by (rule conjunct2)
    have "C = A"
      using ‹A ∈ P› hA hC' by simp
    moreover have "C = B"
      using ‹B ∈ P› hB hC by simp
    ultimately show "A = B"
      by (rule subst)
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by simp
  then have "∃A∈P. x ∈ A ∧ z ∈ A"
    using ‹A ∈ P› by (rule bexI)
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P›
    by (unfold relacion_def)
qed

(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (meson relacion_def)
  obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (meson relacion_def)
  have "A = B"
  proof -
    obtain C where "C ∈ P" and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms particion_def
      by metis
    have "C = A"
      using ‹A ∈ P› hA hC by auto
    moreover have "C = B"
      using ‹B ∈ P› hB hC by auto
    ultimately show "A = B"
      by simp
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by auto
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P› relacion_def
    by metis
qed

(* 3ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
  using assms particion_def relacion_def
  by (smt (verit) transpI)

end

theory Las_particiones_definen_relaciones_transitivas

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where

"particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)

lemma

assumes "particion P"

shows "transp (relacion P)"

proof (rule transpI)

fix x y z

assume "relacion P x y" and "relacion P y z"

have "∃A∈P. x ∈ A ∧ y ∈ A"

using ‹relacion P x y›

by (simp only: relacion_def)

then obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"

by (rule bexE)

have "∃B∈P. y ∈ B ∧ z ∈ B"

using ‹relacion P y z›

by (simp only: relacion_def)

then obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"

by (rule bexE)

have "A = B"

proof -

have "∃C ∈ P. y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

using assms

by (simp only: particion_def)

then obtain C where "C ∈ P"

and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

by (rule bexE)

have hC' : "∀D∈P. y ∈ D ⟶ C = D"

using hC by (rule conjunct2)

have "C = A"

using ‹A ∈ P› hA hC' by simp

moreover have "C = B"

using ‹B ∈ P› hB hC by simp

ultimately show "A = B"

by (rule subst)

qed

then have "x ∈ A ∧ z ∈ A"

using hA hB by simp

then have "∃A∈P. x ∈ A ∧ z ∈ A"

using ‹A ∈ P› by (rule bexI)

then show "relacion P x z"

using ‹A = B› ‹A ∈ P›

by (unfold relacion_def)

qed

(* 2ª demostración *)

lemma

assumes "particion P"

shows "transp (relacion P)"

proof (rule transpI)

fix x y z

assume "relacion P x y" and "relacion P y z"

obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"

using ‹relacion P x y›

by (meson relacion_def)

obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"

using ‹relacion P y z›

by (meson relacion_def)

have "A = B"

proof -

obtain C where "C ∈ P" and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

using assms particion_def

by metis

have "C = A"

using ‹A ∈ P› hA hC by auto

moreover have "C = B"

using ‹B ∈ P› hB hC by auto

ultimately show "A = B"

by simp

qed

then have "x ∈ A ∧ z ∈ A"

using hA hB by auto

then show "relacion P x z"

using ‹A = B› ‹A ∈ P› relacion_def

by metis

qed

(* 3ª demostración *)

lemma

assumes "particion P"

shows "transp (relacion P)"

using assms particion_def relacion_def

by (smt (verit) transpI)

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]

Las familias de conjuntos definen relaciones simétricas

PorJosé A. Alonso 26 agosto 202121 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Demostrar que si P es una familia de subconjunt❙os de X, entonces la relación definida por P es simétrica.

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

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

example : symmetric (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

example : symmetric (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

-- 1ª demostración
example : symmetric (relacion P) :=
begin
  unfold symmetric,
  intros x y hxy,
  unfold relacion at *,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split },
  { exact hBP, },
  { exact hyB, },
  { exact hxB, },
end

-- 2ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split } ;
  assumption,
end

-- 3ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use [B, ⟨hBP, hyB, hxB⟩],
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

-- 1ª demostración

example : symmetric (relacion P) :=

begin

unfold symmetric,

intros x y hxy,

unfold relacion at *,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use B,

repeat { split },

{ exact hBP, },

{ exact hyB, },

{ exact hxB, },

end

-- 2ª demostración

example : symmetric (relacion P) :=

begin

intros x y hxy,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use B,

repeat { split } ;

assumption,

end

-- 3ª demostración

example : symmetric (relacion P) :=

begin

intros x y hxy,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use [B, ⟨hBP, hyB, hxB⟩],

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 Las_familias_de_conjuntos_definen_relaciones_simetricas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

(* 1ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then have "∃A∈P. x ∈ A ∧ y ∈ A"
    by (unfold relacion_def)
  then have "∃A∈P. y ∈ A ∧ x ∈ A"
  proof (rule bexE)
    fix A
    assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A"
    have "y ∈ A ∧ x ∈ A"
      using hA2 by (simp only: conj_commute)
    then show "∃A∈P. y ∈ A ∧ x ∈ A"
      using hA1 by (rule bexI)
  qed
  then show "relacion P y x"
    by (unfold relacion_def)
qed

(* 2ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"
    using relacion_def
    by metis
  then show "relacion P y x"
    using relacion_def
    by metis
qed

(* 3ª demostración *)
lemma "symp (relacion P)"
  using relacion_def
  by (metis sympI)

end

theory Las_familias_de_conjuntos_definen_relaciones_simetricas

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

(* 1ª demostración *)

lemma "symp (relacion P)"

proof (rule sympI)

fix x y

assume "relacion P x y"

then have "∃A∈P. x ∈ A ∧ y ∈ A"

by (unfold relacion_def)

then have "∃A∈P. y ∈ A ∧ x ∈ A"

proof (rule bexE)

fix A

assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A"

have "y ∈ A ∧ x ∈ A"

using hA2 by (simp only: conj_commute)

then show "∃A∈P. y ∈ A ∧ x ∈ A"

using hA1 by (rule bexI)

qed

then show "relacion P y x"

by (unfold relacion_def)

qed

(* 2ª demostración *)

lemma "symp (relacion P)"

proof (rule sympI)

fix x y

assume "relacion P x y"

then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"

using relacion_def

by metis

then show "relacion P y x"

using relacion_def

by metis

qed

(* 3ª demostración *)

lemma "symp (relacion P)"

using relacion_def

by (metis sympI)

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]

Las particiones definen relaciones reflexivas

PorJosé A. Alonso 25 agosto 202119 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada elemento de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

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

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

Demostrar que si P es una partición de X, entonces la relación definida por P es reflexiva.

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

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

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

example
  (h : particion P)
  : reflexive (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

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

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

example

(h : particion P)

: reflexive (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

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

-- 1ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  unfold reflexive,
  intro x,
  unfold relacion,
  unfold particion at h,
  replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,
  rcases h with ⟨A, hAP, hxA, -⟩,
  use A,
  repeat { split },
  { exact hAP, },
  { exact hxA, },
  { exact hxA, },
end

-- 2ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  intro x,
  replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,
  rcases h with ⟨A, hAP, hxA, -⟩,
  use A,
  repeat { split } ; assumption,
end

-- 3ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  intro x,
  rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,
  use A,
  repeat { split } ; assumption,
end

-- 4ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  intro x,
  rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,
  use [A, ⟨hAP, hxA, hxA⟩],
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

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

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

-- 1ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

unfold reflexive,

intro x,

unfold relacion,

unfold particion at h,

replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,

rcases h with ⟨A, hAP, hxA, -⟩,

use A,

repeat { split },

{ exact hAP, },

{ exact hxA, },

end

-- 2ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

intro x,

replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,

rcases h with ⟨A, hAP, hxA, -⟩,

use A,

repeat { split } ; assumption,

end

-- 3ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

intro x,

rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,

use A,

repeat { split } ; assumption,

end

-- 4ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

intro x,

rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,

use [A, ⟨hAP, hxA, hxA⟩],

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 Las_particiones_definen_relaciones_reflexivas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

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

ru(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "reflp (relacion P)"
proof (rule reflpI)
  fix x
  have "(∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"
    using assms by (unfold particion_def)
  then have "∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"
    by (rule conjunct1)
  then have "∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C)"
    by (rule allE)
  then obtain B where "B ∈ P ∧ (x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"
    by (rule someI2_bex)
  then obtain B where "(B ∈ P ∧ x ∈ B) ∧ (∀C∈P. x ∈ C ⟶ B = C)"
    by (simp only: conj_assoc)
  then have "B ∈ P ∧ x ∈ B"
    by (rule conjunct1)
  then have "x ∈ B"
    by (rule conjunct2)
  then have "x ∈ B ∧ x ∈ B"
    using ‹x ∈ B› by (rule conjI)
  moreover have "B ∈ P"
    using ‹B ∈ P ∧ x ∈ B› by (rule conjunct1)
  ultimately have "∃B∈P. x ∈ B ∧ x ∈ B"
    by (rule bexI)
  then show "relacion P x x"
    by (unfold relacion_def)
qed

(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "reflp (relacion P)"
proof (rule reflpI)
  fix x
  obtain A where "A ∈ P ∧ x ∈ A"
    using assms particion_def
    by metis
  then show "relacion P x x"
    using relacion_def
    by metis
qed

(* 3ª demostración *)
lemma
  assumes "particion P"
  shows   "reflp (relacion P)"
  using assms particion_def relacion_def
  by (metis reflp_def)

end

theory Las_particiones_definen_relaciones_reflexivas

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where

"particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

ru(* 1ª demostración *)

lemma

assumes "particion P"

shows "reflp (relacion P)"

proof (rule reflpI)

fix x

have "(∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

using assms by (unfold particion_def)

then have "∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"

by (rule conjunct1)

then have "∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C)"

by (rule allE)

then obtain B where "B ∈ P ∧ (x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"

by (rule someI2_bex)

then obtain B where "(B ∈ P ∧ x ∈ B) ∧ (∀C∈P. x ∈ C ⟶ B = C)"

by (simp only: conj_assoc)

then have "B ∈ P ∧ x ∈ B"

by (rule conjunct1)

then have "x ∈ B"

by (rule conjunct2)

then have "x ∈ B ∧ x ∈ B"

using ‹x ∈ B› by (rule conjI)

moreover have "B ∈ P"

using ‹B ∈ P ∧ x ∈ B› by (rule conjunct1)

ultimately have "∃B∈P. x ∈ B ∧ x ∈ B"

by (rule bexI)

then show "relacion P x x"

by (unfold relacion_def)

qed

(* 2ª demostración *)

lemma

assumes "particion P"

shows "reflp (relacion P)"

proof (rule reflpI)

fix x

obtain A where "A ∈ P ∧ x ∈ A"

using assms particion_def

by metis

then show "relacion P x x"

using relacion_def

by metis

qed

(* 3ª demostración *)

lemma

assumes "particion P"

shows "reflp (relacion P)"

using assms particion_def relacion_def

by (metis reflp_def)

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]

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]

Las clases de equivalencia de elementos no relacionados son disjuntas

PorJosé A. Alonso 23 agosto 202121 agosto 2021

Demostrar que las clases de equivalencia de elementos no relacionados son disjuntas.

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}

example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
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}

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

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}

-- 1ª demostración
example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
begin
  rcases h with ⟨hr, hs, ht⟩,
  by_contradiction h1,
  apply hxy,
  have h2 : ∃ z, z ∈ clase R x ∩ clase R y,
    { contrapose h1,
      intro h1a,
      apply h1a,
      push_neg at h1,
      exact set.eq_empty_iff_forall_not_mem.mpr h1, },
  rcases h2 with ⟨z, hxz, hyz⟩,
  replace hxz : R x z := hxz,
  replace hyz : R y z := hyz,
  have hzy : R z y := hs hyz,
  exact ht hxz hzy,
end

-- 2ª demostración
example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
begin
  rcases h with ⟨hr, hs, ht⟩,
  by_contradiction h1,
  have h2 : ∃ z, z ∈ clase R x ∩ clase R y,
    { by finish [set.eq_empty_iff_forall_not_mem]},
  apply hxy,
  rcases h2 with ⟨z, hxz, hyz⟩,
  exact ht hxz (hs hyz),
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}

-- 1ª demostración

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

begin

rcases h with ⟨hr, hs, ht⟩,

by_contradiction h1,

apply hxy,

have h2 : ∃ z, z ∈ clase R x ∩ clase R y,

{ contrapose h1,

intro h1a,

apply h1a,

push_neg at h1,

exact set.eq_empty_iff_forall_not_mem.mpr h1, },

rcases h2 with ⟨z, hxz, hyz⟩,

replace hxz : R x z := hxz,

replace hyz : R y z := hyz,

have hzy : R z y := hs hyz,

exact ht hxz hzy,

end

-- 2ª demostración

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

begin

rcases h with ⟨hr, hs, ht⟩,

by_contradiction h1,

have h2 : ∃ z, z ∈ clase R x ∩ clase R y,

{ by finish [set.eq_empty_iff_forall_not_mem]},

apply hxy,

rcases h2 with ⟨z, hxz, hyz⟩,

exact ht hxz (hs hyz),

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 Las_clases_de_equivalencia_de_elementos_no_relacionados_son_disjuntas
imports Main
begin

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

(* 1ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
proof -
  have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"
  proof (intro allI impI)
    fix z
    assume "z ∈ clase R x"
    then have "R x z"
      using clase_def by (metis CollectD)
    show "z ∉ clase R y"
    proof (rule notI)
      assume "z ∈ clase R y"
      then have "R y z"
        using clase_def by (metis CollectD)
      then have "R z y"
        using assms(1) by (simp only: equivp_symp)
      with ‹R x z› have "R x y"
        using assms(1) by (simp only: equivp_transp)
      with ‹¬R x y› show False
        by (rule notE)
    qed
  qed
  then show "clase R x ∩ clase R y = {}"
    by (simp only: disjoint_iff)
qed

(* 2ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
proof -
  have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"
  proof (intro allI impI)
    fix z
    assume "z ∈ clase R x"
    then have "R x z"
      using clase_def by fastforce
    show "z ∉ clase R y"
    proof (rule notI)
      assume "z ∈ clase R y"
      then have "R y z"
        using clase_def by fastforce
      then have "R z y"
        using assms(1) by (simp only: equivp_symp)
      with ‹R x z› have "R x y"
        using assms(1) by (simp only: equivp_transp)
      with ‹¬R x y› show False
        by simp
    qed
  qed
  then show "clase R x ∩ clase R y = {}"
    by (simp only: disjoint_iff)
qed

(* 3ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
  using assms
  by (metis clase_def
            CollectD
            equivp_symp
            equivp_transp
            disjoint_iff)

(* 4ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
  using assms
  by (metis equivp_def
            clase_def
            CollectD
            disjoint_iff_not_equal)

end

theory Las_clases_de_equivalencia_de_elementos_no_relacionados_son_disjuntas

imports Main

begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"

where "clase R x = {y. R x y}"

(* 1ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

proof -

have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"

proof (intro allI impI)

fix z

assume "z ∈ clase R x"

then have "R x z"

using clase_def by (metis CollectD)

show "z ∉ clase R y"

proof (rule notI)

assume "z ∈ clase R y"

then have "R y z"

using clase_def by (metis CollectD)

then have "R z y"

using assms(1) by (simp only: equivp_symp)

with ‹R x z› have "R x y"

using assms(1) by (simp only: equivp_transp)

with ‹¬R x y› show False

by (rule notE)

qed

then show "clase R x ∩ clase R y = {}"

by (simp only: disjoint_iff)

qed

(* 2ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

proof -

have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"

proof (intro allI impI)

fix z

assume "z ∈ clase R x"

then have "R x z"

using clase_def by fastforce

show "z ∉ clase R y"

proof (rule notI)

assume "z ∈ clase R y"

then have "R y z"

using clase_def by fastforce

then have "R z y"

using assms(1) by (simp only: equivp_symp)

with ‹R x z› have "R x y"

using assms(1) by (simp only: equivp_transp)

with ‹¬R x y› show False

by simp

qed

then show "clase R x ∩ clase R y = {}"

by (simp only: disjoint_iff)

qed

(* 3ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

using assms

by (metis clase_def

CollectD

equivp_symp

equivp_transp

disjoint_iff)

(* 4ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

using assms

by (metis equivp_def

clase_def

CollectD

disjoint_iff_not_equal)

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]

Las clases de equivalencia de elementos relacionados son iguales

PorJosé A. Alonso 22 agosto 202121 agosto 2021

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

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}

example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
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}

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

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}

-- 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 :=
begin
  intros z hz,
  have hyz : R y z := hz,
  have htrans : transitive R := h.2.2,
  have hxz : R x z := htrans hxy hyz,
  exact hxz,
end

-- 2ª demostración del lema auxiliar
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
begin
  intros z hz,
  exact h.2.2 hxy hz,
end

-- 3ª demostración del lema auxiliar
lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 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 :=
begin
  apply le_antisymm,
  { have hs : symmetric R := h.2.1,
    have hyx : R y x := hs hxy,
    exact aux h hyx, },
  { exact aux h hxy, },
end

-- 2ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
begin
  apply le_antisymm,
  { exact aux h (h.2.1 hxy), },
  { exact aux h hxy, },
end

-- 3ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
le_antisymm (aux h (h.2.1 hxy)) (aux h hxy)

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}

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

begin

intros z hz,

have hyz : R y z := hz,

have htrans : transitive R := h.2.2,

have hxz : R x z := htrans hxy hyz,

exact hxz,

end

-- 2ª demostración del lema auxiliar

example

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

begin

intros z hz,

exact h.2.2 hxy hz,

end

-- 3ª demostración del lema auxiliar

lemma aux

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

λ z hz, h.2.2 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 :=

begin

apply le_antisymm,

{ have hs : symmetric R := h.2.1,

have hyx : R y x := hs hxy,

exact aux h hyx, },

{ exact aux h hxy, },

end

-- 2ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

begin

apply le_antisymm,

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

{ exact aux h hxy, },

end

-- 3ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

le_antisymm (aux h (h.2.1 hxy)) (aux h hxy)

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

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)

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

(* 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

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]

La igualdad de valores es una relación de equivalencia

PorJosé A. Alonso 19 agosto 202110 agosto 2021

Sean X e Y dos conjuntos y f una función de X en Y. Se define la relación R en X de forma que x está relacionado con y si f(x) = f(y).

Demostrar que R es una relación de equivalencia.

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

import tactic

universe u
variables {X Y : Type u}
variable  (f : X → Y)

def R (x y : X) := f x = f y

example : equivalence (R f) :=
sorry

import tactic

universe u

variables {X Y : Type u}

variable (f : X → Y)

def R (x y : X) := f x = f y

example : equivalence (R f) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

universe u
variables {X Y : Type u}
variable  (f : X → Y)

def R (x y : X) := f x = f y

-- 1ª demostración
example : equivalence (R f) :=
begin
  unfold equivalence,
  repeat { split },
  { unfold reflexive,
    intro x,
    unfold R, },
  { unfold symmetric,
    intros x y hxy,
    unfold R,
    exact symm hxy, },
  { unfold transitive,
    unfold R,
    intros x y z hxy hyz,
    exact eq.trans hxy hyz, },
end

-- 2ª demostración
example : equivalence (R f) :=
begin
  repeat { split },
  { intro x,
    exact rfl, },
  { intros x y hxy,
    exact eq.symm hxy, },
  { intros x y z hxy hyz,
    exact eq.trans hxy hyz, },
end

-- 3ª demostración
example : equivalence (R f) :=
begin
  repeat { split },
  { exact λ x, rfl, },
  { exact λ x y hxy, eq.symm hxy, },
  { exact λ x y z hxy hyz, eq.trans hxy hyz, },
end

-- 4ª demostración
example : equivalence (R f) :=
⟨λ x, rfl,
 λ x y hxy, eq.symm hxy,
 λ x y z hxy hyz, eq.trans hxy hyz⟩

import tactic

universe u

variables {X Y : Type u}

variable (f : X → Y)

def R (x y : X) := f x = f y

-- 1ª demostración

example : equivalence (R f) :=

begin

unfold equivalence,

repeat { split },

{ unfold reflexive,

intro x,

unfold R, },

{ unfold symmetric,

intros x y hxy,

unfold R,

exact symm hxy, },

{ unfold transitive,

unfold R,

intros x y z hxy hyz,

exact eq.trans hxy hyz, },

end

-- 2ª demostración

example : equivalence (R f) :=

begin

repeat { split },

{ intro x,

exact rfl, },

{ intros x y hxy,

exact eq.symm hxy, },

{ intros x y z hxy hyz,

exact eq.trans hxy hyz, },

end

-- 3ª demostración

example : equivalence (R f) :=

begin

repeat { split },

{ exact λ x, rfl, },

{ exact λ x y hxy, eq.symm hxy, },

{ exact λ x y z hxy hyz, eq.trans hxy hyz, },

end

-- 4ª demostración

example : equivalence (R f) :=

⟨λ x, rfl,

λ x y hxy, eq.symm hxy,

λ x y z hxy hyz, eq.trans hxy hyz⟩

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 La_igualdad_de_valores_es_una_relacion_de_equivalencia
imports Main
begin

definition R :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where
  "R f x y ⟷ (f x = f y)"

(* 1ª demostración *)
lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
  proof (rule reflpI)
    fix x
    have "f x = f x"
      by (rule refl)
    then show "R f x x"
      by (unfold R_def)
  qed
next
  show "symp (R f)"
  proof (rule sympI)
    fix x y
    assume "R f x y"
    then have "f x = f y"
      by (unfold R_def)
    then have "f y = f x"
      by (rule sym)
    then show "R f y x"
      by (unfold R_def)
  qed
next
  show "transp (R f)"
  proof (rule transpI)
    fix x y z
    assume "R f x y" and "R f y z"
    then have "f x = f y" and "f y = f z"
      by (unfold R_def)
    then have "f x = f z"
      by (rule ssubst)
    then show "R f x z"
      by (unfold R_def)
  qed
qed

(* 2ª demostración *)
lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
  proof (rule reflpI)
    fix x
    show "R f x x"
      by (metis R_def)
  qed
next
  show "symp (R f)"
  proof (rule sympI)
    fix x y
    assume "R f x y"
    then show "R f y x"
      by (metis R_def)
  qed
next
  show "transp (R f)"
  proof (rule transpI)
    fix x y z
    assume "R f x y" and "R f y z"
    then show "R f x z"
      by (metis R_def)
  qed
qed

(* 3ª demostración *)
lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
    by (simp add: R_def reflpI)
next
  show "symp (R f)"
    by (metis R_def sympI)
next
  show "transp (R f)"
    by (metis R_def transpI)
qed

(* 4ª demostración *)
lemma "equivp (R f)"
  by (metis R_def
            equivpI
            reflpI
            sympI
            transpI)

end

theory La_igualdad_de_valores_es_una_relacion_de_equivalencia

imports Main

begin

definition R :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where

"R f x y ⟷ (f x = f y)"

(* 1ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

proof (rule reflpI)

fix x

have "f x = f x"

by (rule refl)

then show "R f x x"

by (unfold R_def)

qed

show "symp (R f)"

proof (rule sympI)

fix x y

assume "R f x y"

then have "f x = f y"

by (unfold R_def)

then have "f y = f x"

by (rule sym)

then show "R f y x"

by (unfold R_def)

qed

show "transp (R f)"

proof (rule transpI)

fix x y z

assume "R f x y" and "R f y z"

then have "f x = f y" and "f y = f z"

by (unfold R_def)

then have "f x = f z"

by (rule ssubst)

then show "R f x z"

by (unfold R_def)

qed

(* 2ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

proof (rule reflpI)

fix x

show "R f x x"

by (metis R_def)

qed

show "symp (R f)"

proof (rule sympI)

fix x y

assume "R f x y"

then show "R f y x"

by (metis R_def)

qed

show "transp (R f)"

proof (rule transpI)

fix x y z

assume "R f x y" and "R f y z"

then show "R f x z"

by (metis R_def)

qed

(* 3ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

by (simp add: R_def reflpI)

show "symp (R f)"

by (metis R_def sympI)

show "transp (R f)"

by (metis R_def transpI)

qed

(* 4ª demostración *)

lemma "equivp (R f)"

by (metis R_def

equivpI

reflpI

sympI

transpI)

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]