principal_neBot_iff

Mathlib.Order.Filter.Basic

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

← MathLib Explorer

English

The principal filter 𝓟(s) is nontrivial if and only if s is nonempty.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem principal_neBot_iff {s : Set α} : NeBot (𝓟 s) ↔ s.Nonempty :=
  neBot_iff.trans <| (not_congr principal_eq_bot_iff).trans nonempty_iff_ne_empty.symm

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

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

Разделы

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

Аффилиация

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