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
    theorem BoundedLENhdsClass.isBounded_le_nhds {α : Type u_7} :
    ∀ {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : BoundedLENhdsClass α] (a : α), Filter.IsBounded (fun (x1 x2 : α) => x1 x2) (nhds a)

    Ad hoc typeclass stating that neighborhoods are eventually bounded below.

    Instances
      theorem BoundedGENhdsClass.isBounded_ge_nhds {α : Type u_7} :
      ∀ {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : BoundedGENhdsClass α] (a : α), Filter.IsBounded (fun (x1 x2 : α) => x1 x2) (nhds a)
      theorem isBounded_le_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] (a : α) :
      Filter.IsBounded (fun (x1 x2 : α) => x1 x2) (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 (x1 x2 : α) => x1 x2) f u
      theorem Filter.Tendsto.bddAbove_range_of_cofinite {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {u : ια} {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
      theorem Filter.Tendsto.bddAbove_range {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] {u : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
      theorem isCobounded_ge_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] (a : α) :
      Filter.IsCobounded (fun (x1 x2 : α) => x1 x2) (nhds a)
      theorem Filter.Tendsto.isCoboundedUnder_ge {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι} {u : ια} {a : α} [f.NeBot] (h : Filter.Tendsto u f (nhds a)) :
      Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) (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 (x1 x2 : α) => x1 x2) f u
      theorem Filter.Tendsto.bddBelow_range_of_cofinite {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {u : ια} {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] (h : Filter.Tendsto u Filter.cofinite (nhds a)) :
      theorem Filter.Tendsto.bddBelow_range {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {a : α} [IsDirected α fun (x1 x2 : α) => x1 x2] {u : α} (h : Filter.Tendsto u Filter.atTop (nhds a)) :
      theorem isCobounded_le_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] (a : α) :
      Filter.IsCobounded (fun (x1 x2 : α) => x1 x2) (nhds a)
      theorem Filter.Tendsto.isCoboundedUnder_le {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι} {u : ια} {a : α} [f.NeBot] (h : Filter.Tendsto u f (nhds a)) :
      Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 x2) 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 100]
      Equations
      • =
      @[instance 100]
      Equations
      • =
      @[instance 100]
      instance OrderTopology.to_BoundedLENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [IsDirected α fun (x1 x2 : α) => x1 x2] [OrderTopology α] :
      Equations
      • =
      @[instance 100]
      instance OrderTopology.to_BoundedGENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [IsDirected α fun (x1 x2 : α) => x1 x2] [OrderTopology α] :
      Equations
      • =
      theorem le_nhds_of_limsSup_eq_limsInf {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} (hl : Filter.IsBounded (fun (x1 x2 : α) => x1 x2) f) (hg : Filter.IsBounded (fun (x1 x2 : α) => x1 x2) f) (hs : f.limsSup = a) (hi : f.limsInf = 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.

      theorem limsSup_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) :
      (nhds a).limsSup = a
      theorem limsInf_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) :
      (nhds a).limsInf = a
      theorem limsInf_eq_of_le_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} [f.NeBot] (h : f nhds a) :
      f.limsInf = a

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

      theorem limsSup_eq_of_le_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} [f.NeBot] (h : f nhds a) :
      f.limsSup = a

      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 : α} [f.NeBot] (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 : α} [f.NeBot] (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 (x1 x2 : α) => x1 x2) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) 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 (x1 x2 : α) => x1 x2) 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} [F.NeBot] {f : RS} (f_decr : Antitone f) (f_cont : ContinuousAt f F.limsSup) (bdd_above : autoParam (Filter.IsBounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) (cobdd : autoParam (Filter.IsCobounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) :
      f F.limsSup = Filter.liminf f F

      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 frequently bounded from below).

      theorem Antitone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [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 (x1 x2 : R) => x1 x2) F a) _auto✝) (cobdd : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) 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 frequently bounded from 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} [F.NeBot] {f : RS} (f_decr : Antitone f) (f_cont : ContinuousAt f F.limsInf) (cobdd : autoParam (Filter.IsCobounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) :
      f F.limsInf = Filter.limsup f F

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

      theorem Antitone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [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)) (cobdd : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) 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 below and frequently bounded from above).

      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} [F.NeBot] {f : RS} (f_incr : Monotone f) (f_cont : ContinuousAt f F.limsSup) (bdd_above : autoParam (Filter.IsBounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) (cobdd : autoParam (Filter.IsCobounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) :
      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).

      theorem Monotone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [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 (x1 x2 : R) => x1 x2) F a) _auto✝) (cobdd : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) 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 frequently bounded from 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} [F.NeBot] {f : RS} (f_incr : Monotone f) (f_cont : ContinuousAt f F.limsInf) (cobdd : autoParam (Filter.IsCobounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x1 x2 : R) => x1 x2) F) _auto✝) :
      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).

      theorem Monotone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [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)) (cobdd : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) 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 below and frequently bounded from above).

      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 ι} [F.NeBot] (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 ι} [F.NeBot] (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 ι} [F.NeBot] (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 ι} [F.NeBot] (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 : ) => kFinset.range n, (s (k + 1)).indicator 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 : ) => kFinset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop}
      theorem limsup_const_add {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [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 (x1 x2 : R) => x1 x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [F.NeBot] [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 (x1 x2 : R) => x1 x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [F.NeBot] [Add R] [ContinuousAdd R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x y] (f : ιR) (c : R) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [F.NeBot] [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) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [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) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ιR) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [F.NeBot] [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 (x1 x2 : R) => x1 x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) 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 ι) [F.NeBot] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ιR) (c : R) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 x2) F f) :
      Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c

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