liminf_ae_eq_of_forall_ae_eq — Mathlib

English

If s_n =ᵐ t for all n, then liminf s atTop =ᵐ t.

Русский

Если s_n =ᵐ t для всех n, то liminf s на atTop равен а.э. t.

LaTeX

$$$\\\\forall n,\\\\ s_n =\\\\!ᵐ[\\\\mu] t \\\\Rightarrow \\\\ liminf (s) atTop =ᵐ[\\\\mu] t$$$

Lean4

theorem liminf_ae_eq_of_forall_ae_eq (s : ℕ → Set α) {t : Set α} (h : ∀ n, s n =ᵐ[μ] t) :
    liminf (α := Set α) s atTop =ᵐ[μ] t :=
  by
  simp only [eventuallyEq_set, ← eventually_countable_forall] at h
  refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_
  simp only [mem_liminf_iff_eventually_mem, hx, eventually_const]

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