Theorems · Theorem · general topology

Monotone.map_limsSup_of_continuousAt

∀ {R : Type u_4} {S : Type u_5} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S] [inst_4 : TopologicalSpace S] [OrderTopology S]
  {F : Filter R} [F.NeBot] {f : R → S},
  Monotone f →
    ContinuousAt f F.limsSup →
      autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) F) Monotone.map_limsSup_of_continuousAt._auto_1 →
        autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F) Monotone.map_limsSup_of_continuousAt._auto_3 →
          f F.limsSup = Filter.limsup f F

A monotone function between (conditionally) complete linear ordered spaces sends a Filter.limsSup to the Filter.limsup of the image if the function is continuous at the limsSup (and the filter is bounded from above and frequently bounded from below).

Defined in

Mathlib.Topology.Order.LiminfLimsup

Cited by

5 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderTopologicalSpaceOrderTopologyConditionallyCompleteLinearOrderTopologicalSpaceOrderTopologyFilter.NeBot