sUnion_classes — Mathlib

English

Let r be an equivalence relation on α. Then the union of its equivalence classes equals the whole set α.

Русский

Пусть r — эквивалентность на α. Тогда объединение всех классов эквивалентности равно всей совокупности α.

LaTeX

$$$\\\\bigcup_{C \\\\in r.classes} C = \\\\alpha$$$

Lean4

@[simp]
theorem sUnion_classes (r : Setoid α) : ⋃₀ r.classes = Set.univ :=
  Set.eq_univ_of_forall fun x => Set.mem_sUnion.2 ⟨{y | r y x}, ⟨x, rfl⟩, Setoid.refl _⟩

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