leAtTop_of_not_NeBot

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

URI: https://scilib.ai/kg/mathlib#SummationFilter.leAtTop_of_not_NeBot

← MathLib Explorer

English

If L is not NeBot, then L is LeAtTop.

Русский

Если L не NeBot, то L LeAtTop.

LaTeX

$$$ \forall {\beta}, \text{ if } \neg L.NeBot \Rightarrow L.LeAtTop$$$

Lean4

theorem leAtTop_of_not_NeBot (L : SummationFilter β) (hL : ¬L.NeBot) : L.LeAtTop :=
  by
  have hLs : L.support = Set.univ := by simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]
  exact ⟨L.support_eq_univ_iff.mp hLs⟩

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

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

Разделы

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

Аффилиация

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