Theorems · Theorem · real analysis

Set.limsup_eq_tendsto_sum_indicator_atTop

∀ {α : Type u_1} {R : Type u_2} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [IsOrderedAddMonoid R]
  [AddLeftStrictMono R] [Archimedean R] {r : R},
  0 < r →
    ∀ (s : ℕ → Set α),
      Filter.limsup s Filter.atTop =
        {ω | Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) Filter.atTop Filter.atTop}

Defined in

Mathlib.Algebra.Order.Archimedean.IndicatorCard

Cited by

1 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidPartialOrderIsOrderedAddMonoidAddLeftStrictMonoArchimedean