English
Elements of a partition are exactly the equivalence classes defined by mkClasses; if s ∈ c and y ∈ s, then s equals the class { x | (mkClasses c H) x y }.
Русский
Элементы разбиения равны эквивалентным классам, определяемым mkClasses: если s ∈ c и y ∈ s, тогда s = { x : α | (mkClasses c H) x y }.
LaTeX
$$If hs: s ∈ c and hy: y ∈ s, then s = { x : α | (Setoid.mkClasses c H).r x y }. $$
Lean4
/-- The equivalence classes of the equivalence relation defined by a set of sets
partitioning α are elements of the set of sets. -/
theorem eqv_class_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {y} : {x | mkClasses c H x y} ∈ c :=
(H y).elim fun _ hc _ => eq_eqv_class_of_mem H hc.1 hc.2 ▸ hc.1
