Relation_Induced_by_Partition_is_Equivalence
Provedequivalence-relationsproofwikiquotient-sets
Let P be a partition of a set S. Let R be the relation induced by P. Then R is an equivalence relation on S.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Order.Disjoint
Formal statement
theorem Relation_Induced_by_Partition_is_Equivalence {α : Type _} (P : Set (Set α)) (hCover : ∀ x : α, ∃ S ∈ P, x ∈ S) (hDisjoint : ∀ S₁ ∈ P, ∀ S₂ ∈ P, S₁ ≠ S₂ → Disjoint S₁ S₂) (hNe : ∀ S ∈ P, Set.Nonempty S) : let R := fun x y => ∃ S ∈ P, x ∈ S ∧ y ∈ S; (∀ x, R x x) ∧ (∀ x y, R x y → R y x) ∧ (∀ x y z, R x y → R y z → R x z) := by sorrySource