tendsto_nhds_atTop_iff — Mathlib

English

For a preorder β, a net f: α → Filter β converges to atTop iff for every y, eventually y is below all f(a) (Ici y ∈ f(a)).

Русский

Для предобраза β, сеть f: α → Filter β сходится к atTop тогда и только тогда, когда для каждого y вернулись элементы выше y в каждое f(a).

LaTeX

$$$\text{Tendsto } f \ l\ (\mathcal{N}(\text{atTop})) \iff \forall y, \ \forall^{\!} a \ in l, \; Ici\ y \in f(a).$$$

Lean4

protected theorem tendsto_nhds_atTop_iff [Preorder β] {l : Filter α} {f : α → Filter β} :
    Tendsto f l (𝓝 atTop) ↔ ∀ y, ∀ᶠ a in l, Ici y ∈ f a := by
  simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]

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