limsup_ae_eq_of_forall_ae_eq — Mathlib

English

If s_n =ᵐ t for every n, then limsup s atTop =ᵐ t.

Русский

Если s_n =ᵐ t для каждого n, то limsup s на atTop равен а.э. t.

LaTeX

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

Lean4

theorem limsup_ae_eq_of_forall_ae_eq (s : ℕ → Set α) {t : Set α} (h : ∀ n, s n =ᵐ[μ] t) :
    limsup (α := Set α) s atTop =ᵐ[μ] t :=
  by
  simp only [eventuallyEq_set, ← eventually_countable_forall] at h
  refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_
  simp [mem_limsup_iff_frequently_mem, hx]
    -- Need to specify `α := Set α` above because of diamond; see https://github.com/leanprover-community/mathlib4/pull/19041

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