smallSets_neBot

Mathlib.Order.Filter.SmallSets

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

← MathLib Explorer

English

Every filter l has a nontrivial smallSets: l.smallSets is NeBot.

Русский

У каждого фильтра l есть ненулевые малые множества: l.smallSets не равно ⊥.

LaTeX

$$$ (\\\\text{l .smallSets}).NeBot $$$

Lean4

instance smallSets_neBot (l : Filter α) : NeBot l.smallSets :=
  by
  refine (lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty
  exact monotone_powerset

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

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

Разделы

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

Аффилиация

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