tendsto_nhds_atBot_iff — Mathlib

English

For a preorder β, Tendsto f l (𝓝 atBot) iff for every y, eventually Iic y ∈ f(a).

Русский

Для предобраза β: Tendsto f l (𝓝 atBot) эквивалентно: для каждого y выполнено, что Iic y ∈ f(a) не позже некоторого момента.

LaTeX

$$$\text{Tendsto } f \ l (𝓝(\text{atBot})) \iff \forall y, \ \forall^{\!} a \ in l, \ Iic y \in f(a).$$$

Lean4

protected theorem tendsto_nhds_atBot_iff [Preorder β] {l : Filter α} {f : α → Filter β} :
    Tendsto f l (𝓝 atBot) ↔ ∀ y, ∀ᶠ a in l, Iic y ∈ f a :=
  @Filter.tendsto_nhds_atTop_iff α βᵒᵈ _ _ _

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