termω⁻ — Mathlib

English

If f1 ≤ f2 as filters, then ω f1 ϕ s is contained in ω f2 ϕ s.

Русский

Если фильтры f1 и f2 удовлетворяют f1 ≤ f2, то ω-предел по f1 для s содержится в ω-пределе по f2.

LaTeX

$$$$\omega f_1\;\varphi\;s \subseteq \omega f_2\;\varphi\;s.$$$$

Lean4

/-- The ω-limit w.r.t. `Filter.atBot`. -/
@[scoped term_parser 1000]
public meta def «termω⁻» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `omegaLimit.«termω⁻» 1024 (ParserDescr.symbol✝ "ω⁻")

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