Theorems · Theorem · general topology

Monotone.map_limsInf_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.limsInf →
      autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) F) Monotone.map_limsInf_of_continuousAt._auto_1 →
        autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) F) Monotone.map_limsInf_of_continuousAt._auto_3 →
          f F.limsInf = Filter.liminf f F

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

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