support_eq_univ

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

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

English

If L has LeAtTop, then its support equals the entire universe.

Русский

Если L имеет LeAtTop, то поддержка L равна вселенному множеству.

LaTeX

$$$ \text{@[simp]} \text{theorem support_eq_univ }(L) [L.LeAtTop] : L.support = univ$$$

Lean4

@[simp]
theorem support_eq_univ (L : SummationFilter β) [L.LeAtTop] : L.support = univ :=
  support_eq_univ_iff.mpr L.le_atTop

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

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

Разделы

Аффилиация

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