instLeAtTopConditional

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

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

← MathLib Explorer

English

The conditional summation filter is LeAtTop.

Русский

Условный суммирующий фильтр является верхним элементом LeAtTop.

LaTeX

$$$\\text{LeAtTop}(\\text{conditional }\\beta)$$$

Lean4

instance : (conditional β).LeAtTop :=
  ⟨support_eq_univ_iff.mp <| by
      simpa [eq_univ_iff_forall, support, -eventually_and] using fun x ↦
        prod_mem_prod (eventually_le_atBot x) (eventually_ge_atTop x)⟩

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

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

Разделы

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

Аффилиация

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