ofColex_bot

Mathlib.Combinatorics.Colex

URI: https://scilib.ai/kg/mathlib#Finset.Colex.ofColex_bot

English

Applying ofColex to the bottom element yields the empty Finset: ofColex(⊥) = ∅.

Русский

Применение ofColex к нижней границе даёт пустое множество: ofColex(⊥) = ∅.

LaTeX

$$$ofColex(\bot) = \emptyset$$$

Lean4

@[simp]
theorem ofColex_bot : ofColex (⊥ : Colex (Finset α)) = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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