neBot_or_eq_bot — Mathlib

English

For any summation filter L, either L is NeBot or its underlying filter is Bot.

Русский

Для любого суммирующего фильтра L либо L не пустой, либо его осн. фильтр равен ⊥.

LaTeX

$$$ \text{neBot_or_eq_bot } (L : SummationFilter \beta) : L.NeBot ∨ L.filter = ⊥$$$

Lean4

theorem neBot_or_eq_bot (L : SummationFilter β) : L.NeBot ∨ L.filter = ⊥ :=
  by
  by_cases h : L.filter = ⊥
  · exact .inr h
  · exact .inl ⟨⟨h⟩⟩

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