instHasSupportOfLeAtTop

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

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

English

If L is LeAtTop, then it has a HasSupport structure.

Русский

Если L ≤ atTop, то L имеет структуру HasSupport.

LaTeX

$$$ \text{instance } (L : SummationFilter \beta) [L.LeAtTop] : HasSupport L $$$

Lean4

instance (L : SummationFilter β) [L.LeAtTop] : HasSupport L :=
  ⟨by simp⟩

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

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

Разделы

Аффилиация

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