Lemmas about liminf and limsup in an order topology. #
theorem
isBounded_le_nhds
{α : Type u}
[SemilatticeSup α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
Filter.IsBounded (fun x x_1 => x ≤ x_1) (nhds a)
theorem
Filter.Tendsto.isBoundedUnder_le
{α : Type u}
{β : Type v}
[SemilatticeSup α]
[TopologicalSpace α]
[OrderTopology α]
{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}
{β : Type v}
[SemilatticeSup α]
[TopologicalSpace α]
[OrderTopology α]
{u : β → α}
{a : α}
(h : Filter.Tendsto u Filter.cofinite (nhds a))
:
theorem
Filter.Tendsto.bddAbove_range
{α : Type u}
[SemilatticeSup α]
[TopologicalSpace α]
[OrderTopology α]
{u : ℕ → α}
{a : α}
(h : Filter.Tendsto u Filter.atTop (nhds a))
:
theorem
isCobounded_ge_nhds
{α : Type u}
[SemilatticeSup α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
Filter.IsCobounded (fun x x_1 => x ≥ x_1) (nhds a)
theorem
Filter.Tendsto.isCoboundedUnder_ge
{α : Type u}
{β : Type v}
[SemilatticeSup α]
[TopologicalSpace α]
[OrderTopology α]
{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
theorem
isBounded_ge_nhds
{α : Type u}
[SemilatticeInf α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
Filter.IsBounded (fun x x_1 => x ≥ x_1) (nhds a)
theorem
Filter.Tendsto.isBoundedUnder_ge
{α : Type u}
{β : Type v}
[SemilatticeInf α]
[TopologicalSpace α]
[OrderTopology α]
{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}
{β : Type v}
[SemilatticeInf α]
[TopologicalSpace α]
[OrderTopology α]
{u : β → α}
{a : α}
(h : Filter.Tendsto u Filter.cofinite (nhds a))
:
theorem
Filter.Tendsto.bddBelow_range
{α : Type u}
[SemilatticeInf α]
[TopologicalSpace α]
[OrderTopology α]
{u : ℕ → α}
{a : α}
(h : Filter.Tendsto u Filter.atTop (nhds a))
:
theorem
isCobounded_le_nhds
{α : Type u}
[SemilatticeInf α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
Filter.IsCobounded (fun x x_1 => x ≤ x_1) (nhds a)
theorem
Filter.Tendsto.isCoboundedUnder_le
{α : Type u}
{β : Type v}
[SemilatticeInf α]
[TopologicalSpace α]
[OrderTopology α]
{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
theorem
le_nhds_of_limsSup_eq_limsInf
{α : Type u}
[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)
:
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}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
Filter.limsSup (nhds a) = a
theorem
limsInf_nhds
{α : Type u}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
(a : α)
:
Filter.limsInf (nhds a) = a
theorem
limsInf_eq_of_le_nhds
{α : Type u}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter α}
{a : α}
[Filter.NeBot f]
(h : f ≤ nhds a)
:
Filter.limsInf f = a
If a filter is converging, its limsup coincides with its limit.
theorem
limsSup_eq_of_le_nhds
{α : Type u}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter α}
{a : α}
[Filter.NeBot f]
:
f ≤ nhds a → Filter.limsSup f = a
If a filter is converging, its liminf coincides with its limit.
theorem
Filter.Tendsto.limsup_eq
{α : Type u}
{β : Type v}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter β}
{u : β → α}
{a : α}
[Filter.NeBot f]
(h : Filter.Tendsto u f (nhds a))
:
Filter.limsup u f = a
If a function has a limit, then its limsup coincides with its limit.
theorem
Filter.Tendsto.liminf_eq
{α : Type u}
{β : Type v}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{f : Filter β}
{u : β → α}
{a : α}
[Filter.NeBot f]
(h : Filter.Tendsto u f (nhds a))
:
Filter.liminf u f = a
If a function has a limit, then its liminf coincides with its limit.
theorem
tendsto_of_liminf_eq_limsup
{α : Type u}
{β : Type v}
[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✝)
:
Filter.Tendsto u f (nhds a)
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}
{β : Type v}
[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✝)
:
Filter.Tendsto u f (nhds a)
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}
{β : Type v}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[DenselyOrdered α]
{f : Filter β}
{u : β → α}
{s : Set α}
(hs : Dense s)
(H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → 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}
{β : Type v}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace.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}
{β : Type v}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace.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}
{β : Type v}
[CompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace.FirstCountableTopology α]
[OrderTopology α]
{f : Filter β}
[CountableInterFilter f]
{u : β → α}
:
@[simp]
theorem
liminf_eq_top
{α : Type u}
{β : Type v}
[CompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace.FirstCountableTopology α]
[OrderTopology α]
{f : Filter β}
[CountableInterFilter f]
{u : β → α}
:
theorem
Antitone.map_limsSup_of_continuousAt
{R : Type u_2}
{S : Type u_3}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[Filter.NeBot F]
{f : R → S}
(f_decr : Antitone f)
(f_cont : ContinuousAt f (Filter.limsSup F))
(bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝)
(bdd_below : autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝)
:
f (Filter.limsSup F) = 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 below).
theorem
Antitone.map_limsup_of_continuousAt
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{F : Filter ι}
[Filter.NeBot F]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_decr : Antitone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.limsup a F))
(bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝)
(bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝)
:
f (Filter.limsup a F) = Filter.liminf (f ∘ a) F
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_2}
{S : Type u_3}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[Filter.NeBot F]
{f : R → S}
(f_decr : Antitone f)
(f_cont : ContinuousAt f (Filter.limsInf F))
(bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝)
(bdd_below : autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝)
:
f (Filter.limsInf F) = 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 above and below).
theorem
Antitone.map_liminf_of_continuousAt
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{F : Filter ι}
[Filter.NeBot F]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_decr : Antitone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.liminf a F))
(bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝)
(bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝)
:
f (Filter.liminf a F) = Filter.limsup (f ∘ a) F
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_2}
{S : Type u_3}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[Filter.NeBot F]
{f : R → S}
(f_incr : Monotone f)
(f_cont : ContinuousAt f (Filter.limsSup F))
(bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝)
(bdd_below : autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝)
:
f (Filter.limsSup F) = 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 below).
theorem
Monotone.map_limsup_of_continuousAt
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{F : Filter ι}
[Filter.NeBot F]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_incr : Monotone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.limsup a F))
(bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝)
(bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝)
:
f (Filter.limsup a F) = Filter.limsup (f ∘ a) F
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_2}
{S : Type u_3}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{F : Filter R}
[Filter.NeBot F]
{f : R → S}
(f_incr : Monotone f)
(f_cont : ContinuousAt f (Filter.limsInf F))
(bdd_above : autoParam (Filter.IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝)
(bdd_below : autoParam (Filter.IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝)
:
f (Filter.limsInf F) = 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 above and below).
theorem
Monotone.map_liminf_of_continuousAt
{ι : Type u_1}
{R : Type u_2}
{S : Type u_3}
{F : Filter ι}
[Filter.NeBot F]
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
[ConditionallyCompleteLinearOrder S]
[TopologicalSpace S]
[OrderTopology S]
{f : R → S}
(f_incr : Monotone f)
(a : ι → R)
(f_cont : ContinuousAt f (Filter.liminf a F))
(bdd_above : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F a) _auto✝)
(bdd_below : autoParam (Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F a) _auto✝)
:
f (Filter.liminf a F) = Filter.liminf (f ∘ a) F
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_2}
[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_2}
[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
{R : Type u_2}
[CompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_3}
(x : R)
{as : ι → R}
(x_lt : ∀ (i : ι), x < as i)
{F : Filter ι}
[Filter.NeBot F]
(as_lim : Filter.Tendsto as F (nhds x))
:
theorem
iUnion_Iic_eq_Iio_of_lt_of_tendsto
{R : Type u_2}
[CompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_3}
(x : R)
{as : ι → R}
(lt_x : ∀ (i : ι), as i < x)
{F : Filter ι}
[Filter.NeBot F]
(as_lim : Filter.Tendsto as F (nhds x))
:
theorem
limsup_eq_tendsto_sum_indicator_nat_atTop
{α : Type u}
(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}
(R : Type u_1)
[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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(F : Filter ι)
[Filter.NeBot F]
[Add R]
[ContinuousAdd R]
[CovariantClass R R (fun x y => x + y) fun x y => x ≤ y]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(F : Filter ι)
[Filter.NeBot F]
[Add R]
[ContinuousAdd R]
[CovariantClass R R (Function.swap fun x y => x + y) fun x y => x ≤ y]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(F : Filter ι)
[Filter.NeBot F]
[Add R]
[ContinuousAdd R]
[CovariantClass R R (fun x y => x + y) fun x y => x ≤ y]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(F : Filter ι)
[Filter.NeBot F]
[Add R]
[ContinuousAdd R]
[CovariantClass R R (Function.swap fun x y => x + y) fun x y => x ≤ y]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(F : Filter ι)
[Filter.NeBot F]
[AddCommSemigroup R]
[Sub R]
[ContinuousSub R]
[OrderedSub R]
[CovariantClass R R (fun x y => x + y) fun x y => x ≤ y]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(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 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(F : Filter ι)
[Filter.NeBot F]
[AddCommSemigroup R]
[Sub R]
[ContinuousSub R]
[OrderedSub R]
[CovariantClass R R (fun x y => x + y) fun x y => x ≤ y]
(f : ι → R)
(c : R)
(bdd_above : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => 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
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
[TopologicalSpace R]
[OrderTopology R]
{ι : Type u_2}
(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 => x ≤ x_1) F f)
(bdd_below : Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) F f)
:
Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
liminf (xᵢ - c) = (liminf xᵢ) - c.