title	date	category	has_math
Las particiones definen relaciones de equivalencia	2024-07-09 06:00:00 UTC+02:00	Relaciones de equivalencia	true

[mathjax]

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

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

Una familia \(P\) 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 Lean4 por

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

Demostrar con Lean4 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 Lean4:

import Mathlib.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) :=
by sorry

1. Demostración en lenguaje natural

Sea \(R\) la relación definida por \(P\). Tenemos que demostrar que \(R\) es reflexiva, simétrica y transitiva.

Para demostrar que \(R\) es reflexiva, sea \(x ∈ X\). Puesto que \(P\) es una partición de \(X\), existe un \(A ∈ P) tal que \(x ∈ A). Por tanto, se tiene que \[ (∃ A ∈ P) [x ∈ A ∧ x ∈ A] \] Luego, \(xRx\).

Para demostrar que \(R\) es simétrica, sean \(x, y ∈ X\) tales que \(xRy\). Entonces, existe \(A\) tal que \[ A ∈ P ∧ x ∈ A ∧ y ∈ A \] Por tanto, \[ A ∈ P ∧ y ∈ A ∧ x ∈ A \] es decir, \(yRx\).

Para demostrar que \(R\) es transitiva, sean \(x, y, z ∈ X\) tales que \(xRy\) e \(yRz\). Entonces, existen \(B_1\) y \(B_2\) tales que \begin{align} &B_1 ∈ P ∧ x ∈ B_1 ∧ y ∈ B_1 \tag{1} \\ &B_2 ∈ P ∧ y ∈ B_2 ∧ z ∈ B_2 \tag{2} \end{align} Si demostramos que \(B_1 = B_2\), se tiene que \[ B_1 ∈ P ∧ x ∈ B_1 ∧ z ∈ B_1 \] y, por tanto, \(xRz\).

Para demostrar que \(B_1 = B_2\), se observa que, por ser \(P\) una partición de \(X\), se tiene \[ (∀ x ∈ X)(∃ B ∈ P)(∀ C ∈ P)[x ∈ C → B = C] \] por tanto, para \(y\), existe un \(B ∈ P\) tal que \[ (∀ C ∈ P)[y ∈ C → B = C] \tag{3} \] Entonces, \begin{align} B_1 &= B &&\text{[de (3) y (1)]} \\ &= B_2 &&\text{[de (3) y (2)]} \end{align}

2. Demostraciones con Lean4

import Mathlib.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) :=
by
  set R := relacion P
  repeat' constructor
  . -- ⊢ ∀ (x : X), R x x
    intro x
    -- x : X
    -- ⊢ R x x
    rcases (h.1 x) with ⟨A, hAP, hxA, -⟩
    -- A : Set X
    -- hAP : A ∈ P
    -- hxA : x ∈ A
    -- ⊢ R x x
    exact ⟨A, ⟨hAP, hxA, hxA⟩⟩
  . -- ⊢ ∀ {x y : X}, R x y → R y x
    intros x y hxy
    -- x y : X
    -- hxy : R x y
    -- ⊢ R y x
    rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩
    -- B : Set X
    -- hBP : B ∈ P
    -- hxB : x ∈ B
    -- hyB : y ∈ B
    exact ⟨B, ⟨hBP, hyB, hxB⟩⟩
  . -- ⊢ ∀ {x y z : X}, R x y → R y z → R x z
    rintro x y z ⟨B1, hB1P, hxB1, hyB1⟩ ⟨B2, hB2P, hyB2, hzB2⟩
    -- x y z : X
    -- B1 : Set X
    -- hB1P : B1 ∈ P
    -- hxB1 : x ∈ B1
    -- hyB1 : y ∈ B1
    -- B2 : Set X
    -- hB2P : B2 ∈ P
    -- hyB2 : y ∈ B2
    -- hzB2 : z ∈ B2
    -- ⊢ R x z
    use B1
    -- ⊢ B1 ∈ P ∧ x ∈ B1 ∧ z ∈ B1
    repeat' constructor
    . -- ⊢ B1 ∈ P
      exact hB1P
    . -- ⊢ x ∈ B1
      exact hxB1
    . -- ⊢ z ∈ B1
      convert hzB2
      -- ⊢ B1 = B2
      rcases (h.1 y) with ⟨B, -, -, hB⟩
      -- B : Set X
      -- hB : ∀ (C : Set X), C ∈ P → y ∈ C → B = C
      exact Eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2)

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

example
  (h : particion P)
  : Equivalence (relacion P) :=
by
  set R := relacion P
  repeat' constructor
  . -- ⊢ ∀ (x : X), R x x
    intro x
    -- x : X
    -- ⊢ R x x
    rcases (h.1 x) with ⟨A, hAP, hxA, -⟩
    -- A : Set X
    -- hAP : A ∈ P
    -- hxA : x ∈ A
    -- ⊢ R x x
    exact ⟨A, ⟨hAP, hxA, hxA⟩⟩
  . -- ⊢ ∀ {x y : X}, R x y → R y x
    intros x y hxy
    -- x y : X
    -- hxy : R x y
    -- ⊢ R y x
    rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩
    -- B : Set X
    -- hBP : B ∈ P
    -- hxB : x ∈ B
    -- hyB : y ∈ B
    exact ⟨B, ⟨hBP, hyB, hxB⟩⟩
  . -- ⊢ ∀ {x y z : X}, R x y → R y z → R x z
    rintro x y z ⟨B1, hB1P, hxB1, hyB1⟩ ⟨B2, hB2P, hyB2, hzB2⟩
    -- x y z : X
    -- B1 : Set X
    -- hB1P : B1 ∈ P
    -- hxB1 : x ∈ B1
    -- hyB1 : y ∈ B1
    -- B2 : Set X
    -- hB2P : B2 ∈ P
    -- hyB2 : y ∈ B2
    -- hzB2 : z ∈ B2
    -- ⊢ R x z
    use B1
    -- ⊢ B1 ∈ P ∧ x ∈ B1 ∧ z ∈ B1
    repeat' constructor
    . -- ⊢ B1 ∈ P
      exact hB1P
    . -- ⊢ x ∈ B1
      exact hxB1
    . -- ⊢ z ∈ B1
      convert hzB2
      -- ⊢ B1 = B2
      rcases (h.1 y) with ⟨B, -, -, hB⟩
      -- B : Set X
      -- hB : ∀ (C : Set X), C ∈ P → y ∈ C → B = C
      exact Eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2)

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

-- variable (x y z : X)
-- #check (Eq.trans : x = y → y = z → x = z)

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

3. Demostraciones 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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Las_particiones_definen_relaciones_de_equivalencia.md

Las_particiones_definen_relaciones_de_equivalencia.md

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL

Files

Las_particiones_definen_relaciones_de_equivalencia.md

Latest commit

History

Las_particiones_definen_relaciones_de_equivalencia.md

File metadata and controls

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

3. Demostraciones con Isabelle/HOL