tendstoInMeasure_iff_norm — Mathlib

English

Equivalent to using the norm distance: TendstoInMeasure is equivalent to Tendsto of μ{x|ε≤‖f_i−g‖} over ε>0.

Русский

Эквивалентно переходу к норме: TendstoInMeasure ⇔ Tendsto μ{x: ε≤‖f_i−g‖}.

LaTeX

$$$TendstoInMeasure μ f l g \\iff ∀ ε>0, Tendsto (i ↦ μ\\{x| ε ≤ ‖f_i x - g x‖\\}) l (𝓝 0)$$$

Lean4

theorem tendstoInMeasure_iff_norm [SeminormedAddCommGroup E] {l : Filter ι} {f : ι → α → E} {g : α → E} :
    TendstoInMeasure μ f l g ↔ ∀ ε, 0 < ε → Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0) := by
  simp_rw [tendstoInMeasure_iff_dist, dist_eq_norm_sub]

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