filter_eq_bot_of_isEmpty

Mathlib.Order.Filter.Basic

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

English

If α is empty, every filter equals the bottom filter.

Русский

Если α пусто, любой фильтр равен нижнему фильтру.

LaTeX

$$$[IsEmpty \ α] \ f = ⊥$$$

Lean4

theorem filter_eq_bot_of_isEmpty [IsEmpty α] (f : Filter α) : f = ⊥ :=
  empty_mem_iff_bot.mp <| univ_mem' isEmptyElim

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

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

Разделы

Аффилиация

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