neBot_iff

Mathlib.Order.Filter.Defs

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

English

A filter f is nontrivial (NeBot f) if and only if f ≠ ⊥.

Русский

Фильтр f ненулевой (NeBot f) тогда и только тогда, когда f ≠ ⊥.

LaTeX

$$$\\mathrm{NeBot}(f) \\iff f \\neq \\perp$$$

Lean4

theorem neBot_iff {f : Filter α} : NeBot f ↔ f ≠ ⊥ :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

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

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

Разделы

Аффилиация

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