Documentation

Mathlib.Topology.Algebra.Order.LiminfLimsup

Lemmas about liminf and limsup in an order topology. #

Main declarations #

Implementation notes #

The same lemmas are true in , ℝ × ℝ, ι → ℝ, EuclideanSpace ι ℝ. To avoid code duplication, we provide an ad hoc axiomatisation of the properties we need.

Ad hoc typeclass stating that neighborhoods are eventually bounded above.

Instances

    Ad hoc typeclass stating that neighborhoods are eventually bounded below.

    Instances
      theorem isBounded_le_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] (a : α) :
      Filter.IsBounded (fun (x x_1 : α) => x x_1) (nhds a)
      theorem Filter.Tendsto.isBoundedUnder_le {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι} {u : ια} {a : α} (h : Filter.Tendsto u f (nhds a)) :
      Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u
      theorem Filter.Tendsto.bddAbove_range_of_cofinite {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {u : ια} {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
      theorem Filter.Tendsto.bddAbove_range {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] {u : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
      theorem isCobounded_ge_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] (a : α) :
      Filter.IsCobounded (fun (x x_1 : α) => x x_1) (nhds a)
      theorem Filter.Tendsto.isCoboundedUnder_ge {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι} {u : ια} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) :
      Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) f u
      instance Pi.instBoundedLENhdsClass {ι : Type u_1} {π : ιType u_6} [Finite ι] [(i : ι) → Preorder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedLENhdsClass (π i)] :
      BoundedLENhdsClass ((i : ι) → π i)
      Equations
      theorem isBounded_ge_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] (a : α) :
      Filter.IsBounded (fun (x x_1 : α) => x x_1) (nhds a)
      theorem Filter.Tendsto.isBoundedUnder_ge {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι} {u : ια} {a : α} (h : Filter.Tendsto u f (nhds a)) :
      Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u
      theorem Filter.Tendsto.bddBelow_range_of_cofinite {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {u : ια} {a : α} [IsDirected α fun (x x_1 : α) => x x_1] (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
      theorem Filter.Tendsto.bddBelow_range {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {a : α} [IsDirected α fun (x x_1 : α) => x x_1] {u : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
      theorem isCobounded_le_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] (a : α) :
      Filter.IsCobounded (fun (x x_1 : α) => x x_1) (nhds a)
      theorem Filter.Tendsto.isCoboundedUnder_le {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι} {u : ια} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) :
      Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) f u
      instance Pi.instBoundedGENhdsClass {ι : Type u_1} {π : ιType u_6} [Finite ι] [(i : ι) → Preorder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedGENhdsClass (π i)] :
      BoundedGENhdsClass ((i : ι) → π i)
      Equations
      instance OrderTopology.to_BoundedLENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [IsDirected α fun (x x_1 : α) => x x_1] [OrderTopology α] :
      Equations
      instance OrderTopology.to_BoundedGENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [IsDirected α fun (x x_1 : α) => x x_1] [OrderTopology α] :
      Equations
      theorem le_nhds_of_limsSup_eq_limsInf {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} (hl : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) (hg : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) (hs : Filter.limsSup f = a) (hi : Filter.limsInf f = a) :
      f nhds a

      If the liminf and the limsup of a filter coincide, then this filter converges to their common value, at least if the filter is eventually bounded above and below.

      If a filter is converging, its limsup coincides with its limit.

      If a filter is converging, its liminf coincides with its limit.

      theorem Filter.Tendsto.limsup_eq {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : βα} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) :

      If a function has a limit, then its limsup coincides with its limit.

      theorem Filter.Tendsto.liminf_eq {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : βα} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) :

      If a function has a limit, then its liminf coincides with its limit.

      theorem tendsto_of_liminf_eq_limsup {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : βα} {a : α} (hinf : Filter.liminf u f = a) (hsup : Filter.limsup u f = a) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :

      If the liminf and the limsup of a function coincide, then the limit of the function exists and has the same value.

      theorem tendsto_of_le_liminf_of_limsup_le {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : βα} {a : α} (hinf : a Filter.liminf u f) (hsup : Filter.limsup u f a) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :

      If a number a is less than or equal to the liminf of a function f at some filter and is greater than or equal to the limsup of f, then f tends to a along this filter.

      theorem tendsto_of_no_upcrossings {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {f : Filter β} {u : βα} {s : Set α} (hs : Dense s) (H : as, bs, a < b¬((∃ᶠ (n : β) in f, u n < a) ∃ᶠ (n : β) in f, b < u n)) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
      ∃ (c : α), Filter.Tendsto u f (nhds c)

      Assume that, for any a < b, a sequence can not be infinitely many times below a and above b. If it is also ultimately bounded above and below, then it has to converge. This even works if a and b are restricted to a dense subset.

      theorem eventually_le_limsup {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : βα} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
      ∀ᶠ (b : β) in f, u b Filter.limsup u f
      theorem eventually_liminf_le {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : βα} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
      ∀ᶠ (b : β) in f, Filter.liminf u f u b
      @[simp]
      theorem limsup_eq_bot {α : Type u_2} {β : Type u_3} [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : βα} :
      @[simp]
      theorem liminf_eq_top {α : Type u_2} {β : Type u_3} [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : βα} :
      theorem Antitone.map_limsSup_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : RS} (f_decr : Antitone f) (f_cont : ContinuousAt f (Filter.limsSup F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :

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

      theorem Antitone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : RS} (f_decr : Antitone f) (a : ιR) (f_cont : ContinuousAt f (Filter.limsup a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :

      A continuous antitone function between (conditionally) complete linear ordered spaces sends a Filter.limsup to the Filter.liminf of the images (if the filter is bounded from above and below).

      theorem Antitone.map_limsInf_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : RS} (f_decr : Antitone f) (f_cont : ContinuousAt f (Filter.limsInf F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :

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

      theorem Antitone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : RS} (f_decr : Antitone f) (a : ιR) (f_cont : ContinuousAt f (Filter.liminf a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :

      A continuous antitone function between (conditionally) complete linear ordered spaces sends a Filter.liminf to the Filter.limsup of the images (if the filter is bounded from above and below).

      theorem Monotone.map_limsSup_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : RS} (f_incr : Monotone f) (f_cont : ContinuousAt f (Filter.limsSup F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :

      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 below).

      theorem Monotone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : RS} (f_incr : Monotone f) (a : ιR) (f_cont : ContinuousAt f (Filter.limsup a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :

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

      theorem Monotone.map_limsInf_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : RS} (f_incr : Monotone f) (f_cont : ContinuousAt f (Filter.limsInf F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x x_1) F) _auto✝) :

      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 above and below).

      theorem Monotone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : RS} (f_incr : Monotone f) (a : ιR) (f_cont : ContinuousAt f (Filter.liminf a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F a) _auto✝) :

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

      theorem iInf_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] {x : R} {as : ιR} (x_le : ∀ (i : ι), x as i) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) :
      ⨅ (i : ι), as i = x
      theorem iSup_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] {x : R} {as : ιR} (le_x : ∀ (i : ι), as i x) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) :
      ⨆ (i : ι), as i = x
      theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (x : R) {as : ιR} (x_lt : ∀ (i : ι), x < as i) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) :
      ⋃ (i : ι), Set.Ici (as i) = Set.Ioi x
      theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (x : R) {as : ιR} (lt_x : ∀ (i : ι), as i < x) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) :
      ⋃ (i : ι), Set.Iic (as i) = Set.Iio x
      theorem limsup_eq_tendsto_sum_indicator_nat_atTop {α : Type u_2} (s : Set α) :
      Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range n) fun (k : ) => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop}
      theorem limsup_eq_tendsto_sum_indicator_atTop {α : Type u_2} (R : Type u_7) [StrictOrderedSemiring R] [Archimedean R] (s : Set α) :
      Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ) => Finset.sum (Finset.range n) fun (k : ) => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop}
      theorem limsup_const_add {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.limsup (fun (i : ι) => c + f i) F = c + Filter.limsup f F

      liminf (c + xᵢ) = c + liminf xᵢ.

      theorem limsup_add_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (Function.swap fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.limsup (fun (i : ι) => f i + c) F = Filter.limsup f F + c

      limsup (xᵢ + c) = (limsup xᵢ) + c.

      theorem liminf_const_add {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.liminf (fun (i : ι) => c + f i) F = c + Filter.liminf f F

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

      theorem liminf_add_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (Function.swap fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.liminf (fun (i : ι) => f i + c) F = Filter.liminf f F + c

      liminf (xᵢ + c) = (liminf xᵢ) + c.

      theorem limsup_const_sub {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.limsup (fun (i : ι) => c - f i) F = c - Filter.liminf f F

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

      theorem limsup_sub_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.limsup (fun (i : ι) => f i - c) F = Filter.limsup f F - c

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

      theorem liminf_const_sub {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.liminf (fun (i : ι) => c - f i) F = c - Filter.limsup f F

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

      theorem liminf_sub_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x x_1) F f) :
      Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c

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