tendsto_lift — Mathlib

English

Tendsto m along l to f.lift g is equivalent to Tendsto m l to each g(s) for s ∈ f.

Русский

Пределы последовательности отображений через подъем эквивалентны пределам по каждому g(s) с s ∈ f.

LaTeX

$$Tendsto m l (f.lift g) \iff \forall s \in f, Tendsto m l (g s)$$

Lean4

theorem tendsto_lift {m : γ → β} {l : Filter γ} : Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s) := by
  simp only [Filter.lift, tendsto_iInf]

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