classes_eqv_classes — Mathlib

English

The equivalence classes partition the type; for every a there exists a unique class containing a.

Русский

Эквивалентные классы образуют разбиение множества; для каждого элемента a существует уникальный класс, содержащий a.

LaTeX

$$$\\forall a, \\exists! b \\in r.classes, a \\in b.$$$

Lean4

/-- Equivalence classes partition the type. -/
theorem classes_eqv_classes {r : Setoid α} (a) : ∃! b ∈ r.classes, a ∈ b :=
  ExistsUnique.intro {x | r x a} ⟨r.mem_classes a, r.refl' _⟩ <|
    by
    rintro y ⟨⟨_, rfl⟩, ha⟩
    ext x
    exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩

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