Theorems · Theorem · general topology

liminf_const_sub

∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : AddCommSemigroup R] [inst_5 : Sub R] [ContinuousSub R]
  [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R),
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f → Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F

liminf (c - xᵢ) = c - limsup xᵢ.

Defined in

Mathlib.Topology.Algebra.Order.LiminfLimsup

Cited by

1 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderTopologicalSpaceOrderTopologyFilter.NeBotAddCommSemigroupSubContinuousSubOrderedSubAddLeftMono