principal_eq_bot_iff

Mathlib.Order.Filter.Basic

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

English

The principal filter 𝓟(s) is the bottom filter ⊥ if and only if s is empty.

Русский

Главный фильтр 𝓟(s) равен нулю тогда и только тогда, когда s пусто.

LaTeX

$$$\\mathcal{P}(s) = \\bot \\iff s = \\emptyset$$$

Lean4

@[simp]
theorem principal_eq_bot_iff {s : Set α} : 𝓟 s = ⊥ ↔ s = ∅ :=
  empty_mem_iff_bot.symm.trans <| mem_principal.trans subset_empty_iff

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

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

Разделы

Аффилиация

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