not_neBot

Mathlib.Order.Filter.Basic

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

English

¬NeBot f iff f = ⊥.

Русский

¬NeBot f эквивалентно f = ⊥.

LaTeX

$$$\\neg \\operatorname{NeBot}(f) \\iff f = \\bot$$$

Lean4

@[simp]
theorem not_neBot {f : Filter α} : ¬f.NeBot ↔ f = ⊥ :=
  neBot_iff.not_left

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

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

Разделы

Аффилиация

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