eq_or_neBot

Mathlib.Order.Filter.Basic

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

← MathLib Explorer

English

Every filter is either bottom or NeBot.

Русский

Каждый фильтр либо равен ⊥, либо небот.

LaTeX

$$$\\text{(eq_or_neBot } f) :\\ f = \\bot \\lor \\operatorname{NeBot}(f)$$$

Lean4

/-- Either `f = ⊥` or `Filter.NeBot f`. This is a version of `eq_or_ne` that uses `Filter.NeBot`
as the second alternative, to be used as an instance. -/
theorem eq_or_neBot (f : Filter α) : f = ⊥ ∨ NeBot f :=
  (eq_or_ne f ⊥).imp_right NeBot.mk

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

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

Разделы

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

Аффилиация

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