tendsto_def — Mathlib

English

Definition of Tendsto: a function f tends to l2 along l1 iff the preimage of every set in l2 lies in l1.

Русский

Определение предела по фильтру: функция f сходится к l2 по фильтру l1 тогда и только тогда, когда предобраз каждой множества из l2 принадлежит l1.

LaTeX

$$$$ \operatorname{Tendsto} f l_1 l_2 \iff \forall s \in l_2, f^{-1}(s) \in l_1 $$$$

Lean4

theorem tendsto_def {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁ :=
  Iff.rfl

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