English
Given a partition c of α and a uniqueness property H: every a ∈ α lies in a unique b ∈ c, one defines a relation r on α by x r y iff for every S ∈ c with x ∈ S we have y ∈ S. This is an equivalence relation whose classes are exactly the blocks coming from c.
Русский
Дана разбиение c множества α и свойство уникальности H: каждое a ∈ α принадлежит одной и только одной частичке в c. Тогда определяем отношение r на α так, что x r y тогда, когда для каждого S ∈ c с x ∈ S выполняется y ∈ S. Это эквивалентность, чьи классы совпадают с блоками разбиения.
LaTeX
$$$r(x,y) \\;\\Longleftrightarrow\\; \\forall S \\in c,\\; x \\in S \\Rightarrow y \\in S.$$$
Lean4
/-- Makes an equivalence relation from a set of sets partitioning α. -/
def mkClasses (c : Set (Set α)) (H : ∀ a, ∃! b ∈ c, a ∈ b) : Setoid α
where
r x y := ∀ s ∈ c, x ∈ s → y ∈ s
iseqv.refl := fun _ _ _ hx => hx
iseqv.symm := fun {x _y} h s hs hy => by
obtain ⟨t, ⟨ht, hx⟩, _⟩ := H x
rwa [eq_of_mem_eqv_class H hs hy ht (h t ht hx)]
iseqv.trans := fun {_x _ _} h1 h2 s hs hx => h2 s hs (h1 s hs hx)
