empty_notMem_classes

Mathlib.Data.Setoid.Partition

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

← MathLib Explorer

English

The empty set is not an equivalence class in any partition.

Русский

Пустое множество не является эквив-классом в любом разбиении.

LaTeX

$$$\\emptyset \\notin r.classes.$$$

Lean4

/-- The empty set is not an equivalence class. -/
theorem empty_notMem_classes {r : Setoid α} : ∅ ∉ r.classes := fun ⟨y, hy⟩ => Set.notMem_empty y <| hy.symm ▸ r.refl' y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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