support — Mathlib

English

The support of a summation filter is the set of elements that lie in all sets eventually contained in the filter.

Русский

Поддержка суммирующего фильтра — множество элементов, которые постепенно принадлежат всем множествам фильтра.

LaTeX

$$$ \text{def } \operatorname{support} (L : SummationFilter \beta) := {b | \forall^\!s \in L.filter, b \in s}$$$

Lean4

/-- The support of a summation filter (its `lim inf`, considered as a filter of sets). -/
def support (L : SummationFilter β) : Set β :=
  {b | ∀ᶠ s in L.filter, b ∈ s}

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