Theorems · Theorem · general topology

tendsto_iSup_of_tendsto_limsup

∀ {ι : Type u_1} {α : Type u_7} {β : Type u_8} [inst : ConditionallyCompleteLattice α] [inst_1 : CompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {u : ι → α → β} {c : β},
  (∀ (i : ι), Filter.Tendsto (u i) Filter.atTop (nhds c)) →
    Filter.Tendsto (fun r => Filter.limsup (fun i => u i r) Filter.cofinite) Filter.atTop (nhds c) →
      (∀ (i : ι), Antitone (u i)) → Filter.Tendsto (fun r => ⨆ i, u i r) Filter.atTop (nhds c)

Let u : ι → α → β be a sequence of antitone functions α → β indexed by ι. Suppose that for all i : ι, u i tends to c at infinity, and that furthermore the limsup of i ↦ u i r along the cofinite filter tends to the same c as r tends to infinity. Then the supremum function r ↦ ⨆ i, u i r also tends to c at infinity.

Defined in

Mathlib.Topology.Order.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLatticeCompleteLinearOrderTopologicalSpaceOrderTopology