subsingleton_bot

Mathlib.Order.Filter.Subsingleton

URI: https://scilib.ai/kg/mathlib#Filter.subsingleton_bot

English

The bottom filter ⊥ is subsingleton.

Русский

Нижний фильтр ⊥ является подсинглетным.

LaTeX

$$$$ Filter.Subsingleton(\perp) $$$$

Lean4

@[simp]
theorem subsingleton_bot : Filter.Subsingleton (⊥ : Filter α) :=
  ⟨∅, trivial, subsingleton_empty⟩

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

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

Разделы

Аффилиация

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