tendsto_lift' — Mathlib

English

Let m: γ → β and l be a filter on γ. Then Tendsto m l (f.lift' h) is equivalent to for every s ∈ f, m a eventually lies in h s.

Русский

Пусть m: γ → β и l — фильтр на γ. Тогда Tendsto m l (f.lift' h) эквивалентно тому, что для каждого s ∈ f выполняется: для почти всех a по l, m(a) ∈ h s.

LaTeX

$$$\\mathrm{Tendsto}\\ m\\ l\\ (f.lift' h) \\ \\iff\\ \\forall s \\in f,\\ \\forall^\\infty a \\text{ in } l,\\ m\\,a \\in h\\,s$$$

Lean4

theorem tendsto_lift' {m : γ → β} {l : Filter γ} : Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ a in l, m a ∈ h s := by
  simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]

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