octubre 2021 – Página 3

Las clases de equivalencia son no vacías

PorJosé A. Alonso 5 octubre 20212 octubre 2021

Este ejercicio es el 6º 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.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.

El conjuntos de las clases correspondientes a una relación R se define en Lean por

    def clases : (A → A → Prop) → set (set A) :=
      λ R, {B : set A | ∃ x : A, B = clase R x}

1 2	def clases : (A → A → Prop) → set (set A) := λ R, {B : set A \| ∃ x : A, B = clase R x}

El ejercicio consiste en demostrar que si C es una clase de equivalencia de R, entonces C es no vacía.

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}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

example
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
sorry

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

example

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

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}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

-- Se usará el siguientes 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)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  intros X hX,
  unfold clases at hX,
  dsimp at hX,
  cases hX with a ha,
  rw ha,
  rw set.nonempty_def,
  use a,
  rw pertenece_clase_syss,
  rcases hR with ⟨hrefl, -, -⟩,
  exact hrefl a,
end

-- 2ª demostración
example
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  exact hR.1 a,
end

-- 3ª demostración
example
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

-- 4ª demostración
lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  exact (pertenece_clase_syss R).mpr (hR.1 a),
end

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

-- Se usará el siguientes 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)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

intros X hX,

unfold clases at hX,

dsimp at hX,

cases hX with a ha,

rw ha,

rw set.nonempty_def,

use a,

rw pertenece_clase_syss,

rcases hR with ⟨hrefl, -, -⟩,

exact hrefl a,

end

-- 2ª demostración

example

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

exact hR.1 a,

end

-- 3ª demostración

example

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

-- 4ª demostración

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

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

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]

Las clases de equivalencia son iguales a las de sus elementos

PorJosé A. Alonso 4 octubre 20212 octubre 2021

Este ejercicio es el 5º 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.

El ejercicio consiste en demostrar que si C es una clase de equivalencia y a ∈ C, entonces la clase de equivalencia de a es 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án los siguientes dos lemas auxiliares
lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma subclase_si_pertenece
  {R : A → A → Prop}
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
λ hab z hza, hR.2.2 hza hab

-- 1ª demostración
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a = clase R b :=
begin
  intro hab,
  apply set.subset.antisymm,
  { apply subclase_si_pertenece hR hab, },
  { apply subclase_si_pertenece hR,
    rcases hR with ⟨-, hsymm, -⟩,
    exact hsymm hab }
end

-- 2ª demostración
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a = clase R b :=
begin
  intro hab,
  apply set.subset.antisymm,
  { exact subclase_si_pertenece hR hab, },
  { exact subclase_si_pertenece hR (hR.2.1 hab), }
end

-- 3ª demostración
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a = clase R b :=
begin
  intro hab,
  exact set.subset.antisymm
         (subclase_si_pertenece hR hab)
         (subclase_si_pertenece hR (hR.2.1 hab))
end

-- 4ª demostración
lemma clases_iguales_si_pertenece
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a = clase R b :=
λ hab, set.subset.antisymm
        (subclase_si_pertenece hR hab)
        (subclase_si_pertenece hR (hR.2.1 hab))

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

-- Se usarán los siguientes dos lemas auxiliares

lemma pertenece_clase_syss

{a b : A}

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

by refl

lemma subclase_si_pertenece

{R : A → A → Prop}

(hR: equivalence R)

{a b : A}

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

λ hab z hza, hR.2.2 hza hab

-- 1ª demostración

example

(hR: equivalence R)

{a b : A}

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

begin

intro hab,

apply set.subset.antisymm,

{ apply subclase_si_pertenece hR hab, },

{ apply subclase_si_pertenece hR,

rcases hR with ⟨-, hsymm, -⟩,

exact hsymm hab }

end

-- 2ª demostración

example

(hR: equivalence R)

{a b : A}

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

begin

intro hab,

apply set.subset.antisymm,

{ exact subclase_si_pertenece hR hab, },

{ exact subclase_si_pertenece hR (hR.2.1 hab), }

end

-- 3ª demostración

example

(hR: equivalence R)

{a b : A}

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

begin

intro hab,

exact set.subset.antisymm

(subclase_si_pertenece hR hab)

(subclase_si_pertenece hR (hR.2.1 hab))

end

-- 4ª demostración

lemma clases_iguales_si_pertenece

(hR: equivalence R)

{a b : A}

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

λ hab, set.subset.antisymm

(subclase_si_pertenece hR hab)

(subclase_si_pertenece hR (hR.2.1 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]

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.

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]

Pertenencia a bloques de una partición con elementos comunes

PorJosé A. Alonso 1 octubre 20212 octubre 2021

Este ejercicio es el 2º 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.

El anterior es Igualdad de bloques de una partición cuando tienen elementos comunes.

El ejercicio consiste en demostrar que si dos bloques de una partición tienen elementos comunes, entonces los elementos de uno también pertenecen al otro.

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

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
sorry

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

-- 1ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  apply iguales_si_comun hY hX haY,
  exact haX,
end

-- 2ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  have hXY : X = Y := iguales_si_comun hX hY haX haY,
  rw ← hXY,
  exact hbX,
end

-- 3ª demostración
lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

-- 1ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

apply iguales_si_comun hY hX haY,

exact haX,

end

-- 2ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

have hXY : X = Y := iguales_si_comun hX hY haX haY,

rw ← hXY,

exact hbX,

end

-- 3ª demostración

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

end particion

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]