classes_mkClasses — Mathlib

English

The equivalence classes of the equivalence relation defined by a partition c equals c.

Русский

Классы эквивалентности, порожденные разбиением c, равны самому разбиению c.

LaTeX

$$$ (\\\\operatorname{mkClasses} c \\\\; hc).\\\\classes = c $$$

Lean4

/-- The equivalence classes of the equivalence relation defined by a partition of α equal
the original partition. -/
theorem classes_mkClasses (c : Set (Set α)) (hc : IsPartition c) : (mkClasses c hc.2).classes = c :=
  by
  ext s
  constructor
  · rintro ⟨y, rfl⟩
    obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y
    rwa [← eq_eqv_class_of_mem _ hb hy]
  · exact exists_of_mem_partition hc

Похожие утверждения