isPartition_classes

Mathlib.Data.Setoid.Partition

URI: https://scilib.ai/kg/mathlib#Setoid.isPartition_classes

English

The collection of equivalence classes r.classes forms a partition of α.

Русский

Множество классов эквивалентности r.classes образует разбиение α.

LaTeX

$$$\\text{IsPartition}(r.classes)$$$

Lean4

theorem isPartition_classes (r : Setoid α) : IsPartition r.classes :=
  ⟨empty_notMem_classes, classes_eqv_classes⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru