tendsto_iff — Mathlib

English

If la has basis pa sa and lb has basis pb sb, then Tendsto f la lb is equivalent to: for every ib with pb ib there exists ia with pa ia and ∀ x ∈ sa ia, f x ∈ sb ib.

Русский

Пусть у la базис pa sa, а у lb — pb sb. Тогда Tendsto f la lb эквивалентно: для каждого ib с pb ib существует ia с pa ia и для всех x ∈ sa ia выполняется f x ∈ sb ib.

LaTeX

$$$ \mathrm{Tendsto} f\ la lb \iff \forall ib, pb ib \to \exists ia,\ pa ia \land \forall x \in sa ia, f x \in sb ib $$$

Lean4

theorem tendsto_iff (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
    Tendsto f la lb ↔ ∀ ib, pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib := by
  simp [hlb.tendsto_right_iff, hla.eventually_iff]

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