Skip to main content

Las particiones definen relaciones reflexivas

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

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

Demostrar con Lean4 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 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)
  : Reflexive (relacion P) :=
by sorry

1. Demostración en lenguaje natural

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, \(x\) está relacionado con \(x\) mediante la relación definida por \(P\).

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

-- 1ª demostración
-- ===============

example
  (h : particion P)
  : Reflexive (relacion P) :=
by
  intro x
  -- x : X
  -- ⊢ relacion P x x
  rcases h.1 x with ⟨A, hAP, hxA, -⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  exact ⟨A, hAP, hxA, hxA⟩

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

example
  (h : particion P)
  : Reflexive (relacion P) :=
by
  unfold Reflexive
  -- ⊢ ∀ (x : X), relacion P x x
  intro x
  -- x : X
  -- ⊢ relacion P x x
  unfold relacion
  -- ⊢ ∃ A, A ∈ P ∧ x ∈ A ∧ x ∈ A
  unfold particion at h
  -- h : (∀ x, ∃ B, B ∈ P ∧ x ∈ B ∧ ∀ C, C ∈ P → x ∈ C → B = C) ∧ ¬∅ ∈ P
  replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x
  rcases h with ⟨A, hAP, hxA, -⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  use A

-- 3ª demostración
-- ===============

example
  (h : particion P)
  : Reflexive (relacion P) :=
by
  intro x
  -- ⊢ relacion P x x
  replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x
  rcases h with ⟨A, hAP, hxA, -⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  use A

-- 4ª demostración
-- ===============

example
  (h : particion P)
  : Reflexive (relacion P) :=
by
  intro x
  -- x : X
  -- ⊢ relacion P x x
  rcases (h.1 x) with ⟨A, hAP, hxA, -⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  use A

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

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

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