# mathlib3documentation

order.liminf_limsup

# liminfs and limsups of functions and filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Defines the Liminf/Limsup of a function taking values in a conditionally complete lattice, with respect to an arbitrary filter.

We define `Limsup f` (`Liminf f`) where `f` is a filter taking values in a conditionally complete lattice. `Limsup f` is the smallest element `a` such that, eventually, `u ≤ a` (and vice versa for `Liminf f`). To work with the Limsup along a function `u` use `Limsup (map u f)`.

Usually, one defines the Limsup as `Inf (Sup s)` where the Inf is taken over all sets in the filter. For instance, in ℕ along a function `u`, this is `Inf_n (Sup_{k ≥ n} u k)` (and the latter quantity decreases with `n`, so this is in fact a limit.). There is however a difficulty: it is well possible that `u` is not bounded on the whole space, only eventually (think of `Limsup (λx, 1/x)` on ℝ. Then there is no guarantee that the quantity above really decreases (the value of the `Sup` beforehand is not really well defined, as one can not use ∞), so that the Inf could be anything. So one can not use this `Inf Sup ...` definition in conditionally complete lattices, and one has to use a less tractable definition.

In conditionally complete lattices, the definition is only useful for filters which are eventually bounded above (otherwise, the Limsup would morally be +∞, which does not belong to the space) and which are frequently bounded below (otherwise, the Limsup would morally be -∞, which is not in the space either). We start with definitions of these concepts for arbitrary filters, before turning to the definitions of Limsup and Liminf.

In complete lattices, however, it coincides with the `Inf Sup` definition.

def filter.is_bounded {α : Type u_1} (r : α α Prop) (f : filter α) :
Prop

`f.is_bounded (≺)`: the filter `f` is eventually bounded w.r.t. the relation `≺`, i.e. eventually, it is bounded by some uniform bound. `r` will be usually instantiated with `≤` or `≥`.

Equations
def filter.is_bounded_under {α : Type u_1} {β : Type u_2} (r : α α Prop) (f : filter β) (u : β α) :
Prop

`f.is_bounded_under (≺) u`: the image of the filter `f` under `u` is eventually bounded w.r.t. the relation `≺`, i.e. eventually, it is bounded by some uniform bound.

Equations
• = f)
theorem filter.is_bounded_iff {α : Type u_1} {r : α α Prop} {f : filter α} :
(s : set α) (H : s f.sets) (b : α), s {x : α | r x b}

`f` is eventually bounded if and only if, there exists an admissible set on which it is bounded.

theorem filter.is_bounded_under_of {α : Type u_1} {β : Type u_2} {r : α α Prop} {f : filter β} {u : β α} :
( (b : α), (x : β), r (u x) b)

A bounded function `u` is in particular eventually bounded.

theorem filter.is_bounded_bot {α : Type u_1} {r : α α Prop} :
theorem filter.is_bounded_top {α : Type u_1} {r : α α Prop} :
(t : α), (x : α), r x t
theorem filter.is_bounded_principal {α : Type u_1} {r : α α Prop} (s : set α) :
(t : α), (x : α), x s r x t
theorem filter.is_bounded_sup {α : Type u_1} {r : α α Prop} {f g : filter α} [ r] (hr : (b₁ b₂ : α), (b : α), r b₁ b r b₂ b) :
(f g)
theorem filter.is_bounded.mono {α : Type u_1} {r : α α Prop} {f g : filter α} (h : f g) :
theorem filter.is_bounded_under.mono {α : Type u_1} {β : Type u_2} {r : α α Prop} {f g : filter β} {u : β α} (h : f g) :
theorem filter.is_bounded_under.mono_le {α : Type u_1} {β : Type u_2} [preorder β] {l : filter α} {u v : α β} (hu : u) (hv : v ≤ᶠ[l] u) :
theorem filter.is_bounded_under.mono_ge {α : Type u_1} {β : Type u_2} [preorder β] {l : filter α} {u v : α β} (hu : u) (hv : u ≤ᶠ[l] v) :
theorem filter.is_bounded_under_const {α : Type u_1} {β : Type u_2} {r : α α Prop} [ r] {l : filter β} {a : α} :
(λ (_x : β), a)
theorem filter.is_bounded.is_bounded_under {α : Type u_1} {β : Type u_2} {r : α α Prop} {f : filter α} {q : β β Prop} {u : α β} (hf : (a₀ a₁ : α), r a₀ a₁ q (u a₀) (u a₁)) :
theorem filter.not_is_bounded_under_of_tendsto_at_top {α : Type u_1} {β : Type u_2} [preorder β] [no_max_order β] {f : α β} {l : filter α} [l.ne_bot] (hf : filter.at_top) :
theorem filter.not_is_bounded_under_of_tendsto_at_bot {α : Type u_1} {β : Type u_2} [preorder β] [no_min_order β] {f : α β} {l : filter α} [l.ne_bot] (hf : filter.at_bot) :
theorem filter.is_bounded_under.bdd_above_range_of_cofinite {α : Type u_1} {β : Type u_2} [preorder β] {f : α β}  :
theorem filter.is_bounded_under.bdd_below_range_of_cofinite {α : Type u_1} {β : Type u_2} [preorder β] [ ge] {f : α β}  :
theorem filter.is_bounded_under.bdd_above_range {β : Type u_2} [preorder β] {f : β}  :
theorem filter.is_bounded_under.bdd_below_range {β : Type u_2} [preorder β] [ ge] {f : β}  :
def filter.is_cobounded {α : Type u_1} (r : α α Prop) (f : filter α) :
Prop

`is_cobounded (≺) f` states that the filter `f` does not tend to infinity w.r.t. `≺`. This is also called frequently bounded. Will be usually instantiated with `≤` or `≥`.

There is a subtlety in this definition: we want `f.is_cobounded` to hold for any `f` in the case of complete lattices. This will be relevant to deduce theorems on complete lattices from their versions on conditionally complete lattices with additional assumptions. We have to be careful in the edge case of the trivial filter containing the empty set: the other natural definition `¬ ∀ a, ∀ᶠ n in f, a ≤ n` would not work as well in this case.

Equations
def filter.is_cobounded_under {α : Type u_1} {β : Type u_2} (r : α α Prop) (f : filter β) (u : β α) :
Prop

`is_cobounded_under (≺) f u` states that the image of the filter `f` under the map `u` does not tend to infinity w.r.t. `≺`. This is also called frequently bounded. Will be usually instantiated with `≤` or `≥`.

Equations
• = f)
theorem filter.is_cobounded.mk {α : Type u_1} {r : α α Prop} {f : filter α} [ r] (a : α) (h : (s : set α), s f ( (x : α) (H : x s), r a x)) :

To check that a filter is frequently bounded, it suffices to have a witness which bounds `f` at some point for every admissible set.

This is only an implication, as the other direction is wrong for the trivial filter.

theorem filter.is_bounded.is_cobounded_flip {α : Type u_1} {r : α α Prop} {f : filter α} [ r] [f.ne_bot] :
f

A filter which is eventually bounded is in particular frequently bounded (in the opposite direction). At least if the filter is not trivial.

theorem filter.is_bounded.is_cobounded_ge {α : Type u_1} {f : filter α} [preorder α] [f.ne_bot] (h : f) :
theorem filter.is_bounded.is_cobounded_le {α : Type u_1} {f : filter α} [preorder α] [f.ne_bot] (h : f) :
theorem filter.is_cobounded_bot {α : Type u_1} {r : α α Prop} :
(b : α), (x : α), r b x
theorem filter.is_cobounded_top {α : Type u_1} {r : α α Prop} :
theorem filter.is_cobounded_principal {α : Type u_1} {r : α α Prop} (s : set α) :
(b : α), (a : α), ( (x : α), x s r x a) r b a
theorem filter.is_cobounded.mono {α : Type u_1} {r : α α Prop} {f g : filter α} (h : f g) :
theorem filter.is_bounded_le_at_bot {α : Type u_1} [preorder α] [nonempty α] :
theorem filter.is_bounded_ge_at_top {α : Type u_1} [preorder α] [nonempty α] :
theorem filter.tendsto.is_bounded_under_le_at_bot {α : Type u_1} {β : Type u_2} [preorder α] [nonempty α] {f : filter β} {u : β α} (h : filter.at_bot) :
theorem filter.tendsto.is_bounded_under_ge_at_top {α : Type u_1} {β : Type u_2} [preorder α] [nonempty α] {f : filter β} {u : β α} (h : filter.at_top) :
theorem filter.bdd_below_range_of_tendsto_at_top_at_top {α : Type u_1} [preorder α] [nonempty α] [ ge] {u : α}  :
theorem filter.is_cobounded_le_of_bot {α : Type u_1} [preorder α] [order_bot α] {f : filter α} :
theorem filter.is_cobounded_ge_of_top {α : Type u_1} [preorder α] [order_top α] {f : filter α} :
theorem filter.is_bounded_le_of_top {α : Type u_1} [preorder α] [order_top α] {f : filter α} :
theorem filter.is_bounded_ge_of_bot {α : Type u_1} [preorder α] [order_bot α] {f : filter α} :
@[simp]
theorem order_iso.is_bounded_under_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] (e : α ≃o β) {l : filter γ} {u : γ α} :
(λ (x : γ), e (u x))
@[simp]
theorem order_iso.is_bounded_under_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] (e : α ≃o β) {l : filter γ} {u : γ α} :
(λ (x : γ), e (u x))
@[simp]
theorem filter.is_bounded_under_le_neg {α : Type u_1} {β : Type u_2} {l : filter β} {u : β α} :
(λ (x : β), -u x)
@[simp]
theorem filter.is_bounded_under_le_inv {α : Type u_1} {β : Type u_2} {l : filter β} {u : β α} :
(λ (x : β), (u x)⁻¹)
@[simp]
theorem filter.is_bounded_under_ge_inv {α : Type u_1} {β : Type u_2} {l : filter β} {u : β α} :
(λ (x : β), (u x)⁻¹)
@[simp]
theorem filter.is_bounded_under_ge_neg {α : Type u_1} {β : Type u_2} {l : filter β} {u : β α} :
(λ (x : β), -u x)
theorem filter.is_bounded_under.sup {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β α} :
(λ (a : β), u a v a)
@[simp]
theorem filter.is_bounded_under_le_sup {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β α} :
(λ (a : β), u a v a)
theorem filter.is_bounded_under.inf {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β α} :
(λ (a : β), u a v a)
@[simp]
theorem filter.is_bounded_under_ge_inf {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β α} :
(λ (a : β), u a v a)
theorem filter.is_bounded_under_le_abs {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
(λ (a : β), |u a|)

Filters are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic `is_bounded_default` in the statements, in the form `(hf : f.is_bounded (≥) . is_bounded_default)`.

def filter.Limsup {α : Type u_1} (f : filter α) :
α

The `Limsup` of a filter `f` is the infimum of the `a` such that, eventually for `f`, holds `x ≤ a`.

Equations
def filter.Liminf {α : Type u_1} (f : filter α) :
α

The `Liminf` of a filter `f` is the supremum of the `a` such that, eventually for `f`, holds `x ≥ a`.

Equations
def filter.limsup {α : Type u_1} {β : Type u_2} (u : β α) (f : filter β) :
α

The `limsup` of a function `u` along a filter `f` is the infimum of the `a` such that, eventually for `f`, holds `u x ≤ a`.

Equations
def filter.liminf {α : Type u_1} {β : Type u_2} (u : β α) (f : filter β) :
α

The `liminf` of a function `u` along a filter `f` is the supremum of the `a` such that, eventually for `f`, holds `u x ≥ a`.

Equations
def filter.blimsup {α : Type u_1} {β : Type u_2} (u : β α) (f : filter β) (p : β Prop) :
α

The `blimsup` of a function `u` along a filter `f`, bounded by a predicate `p`, is the infimum of the `a` such that, eventually for `f`, `u x ≤ a` whenever `p x` holds.

Equations
def filter.bliminf {α : Type u_1} {β : Type u_2} (u : β α) (f : filter β) (p : β Prop) :
α

The `bliminf` of a function `u` along a filter `f`, bounded by a predicate `p`, is the supremum of the `a` such that, eventually for `f`, `a ≤ u x` whenever `p x` holds.

Equations
theorem filter.limsup_eq {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
= has_Inf.Inf {a : α | ∀ᶠ (n : β) in f, u n a}
theorem filter.liminf_eq {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
= has_Sup.Sup {a : α | ∀ᶠ (n : β) in f, a u n}
theorem filter.blimsup_eq {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {p : β Prop} :
p = has_Inf.Inf {a : α | ∀ᶠ (x : β) in f, p x u x a}
theorem filter.bliminf_eq {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {p : β Prop} :
p = has_Sup.Sup {a : α | ∀ᶠ (x : β) in f, p x a u x}
@[simp]
theorem filter.blimsup_true {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) :
(λ (x : β), true) =
@[simp]
theorem filter.bliminf_true {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) :
(λ (x : β), true) =
theorem filter.blimsup_eq_limsup_subtype {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {p : β Prop} :
theorem filter.bliminf_eq_liminf_subtype {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {p : β Prop} :
theorem filter.Limsup_le_of_le {α : Type u_1} {f : filter α} {a : α} (hf : . "is_bounded_default") (h : ∀ᶠ (n : α) in f, n a) :
theorem filter.le_Liminf_of_le {α : Type u_1} {f : filter α} {a : α} (hf : . "is_bounded_default") (h : ∀ᶠ (n : α) in f, a n) :
theorem filter.limsup_le_of_le {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {a : α} (hf : . "is_bounded_default") (h : ∀ᶠ (n : β) in f, u n a) :
a
theorem filter.le_liminf_of_le {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {a : α} (hf : . "is_bounded_default") (h : ∀ᶠ (n : β) in f, a u n) :
a
theorem filter.le_Limsup_of_le {α : Type u_1} {f : filter α} {a : α} (hf : . "is_bounded_default") (h : (b : α), (∀ᶠ (n : α) in f, n b) a b) :
theorem filter.Liminf_le_of_le {α : Type u_1} {f : filter α} {a : α} (hf : . "is_bounded_default") (h : (b : α), (∀ᶠ (n : α) in f, b n) b a) :
theorem filter.le_limsup_of_le {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {a : α} (hf : . "is_bounded_default") (h : (b : α), (∀ᶠ (n : β) in f, u n b) a b) :
a
theorem filter.liminf_le_of_le {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} {a : α} (hf : . "is_bounded_default") (h : (b : α), (∀ᶠ (n : β) in f, b u n) b a) :
a
theorem filter.Liminf_le_Limsup {α : Type u_1} {f : filter α} [f.ne_bot] (h₁ : . "is_bounded_default") (h₂ : . "is_bounded_default") :
theorem filter.liminf_le_limsup {α : Type u_1} {β : Type u_2} {f : filter β} [f.ne_bot] {u : β α} (h : . "is_bounded_default") (h' : . "is_bounded_default") :
theorem filter.Limsup_le_Limsup {α : Type u_1} {f g : filter α} (hf : . "is_bounded_default") (hg : . "is_bounded_default") (h : (a : α), (∀ᶠ (n : α) in g, n a) (∀ᶠ (n : α) in f, n a)) :
theorem filter.Liminf_le_Liminf {α : Type u_1} {f g : filter α} (hf : . "is_bounded_default") (hg : . "is_bounded_default") (h : (a : α), (∀ᶠ (n : α) in f, a n) (∀ᶠ (n : α) in g, a n)) :
theorem filter.limsup_le_limsup {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α β} (h : u ≤ᶠ[f] v) (hu : . "is_bounded_default") (hv : . "is_bounded_default") :
theorem filter.liminf_le_liminf {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α β} (h : ∀ᶠ (a : α) in f, u a v a) (hu : . "is_bounded_default") (hv : . "is_bounded_default") :
theorem filter.Limsup_le_Limsup_of_le {α : Type u_1} {f g : filter α} (h : f g) (hf : . "is_bounded_default") (hg : . "is_bounded_default") :
theorem filter.Liminf_le_Liminf_of_le {α : Type u_1} {f g : filter α} (h : g f) (hf : . "is_bounded_default") (hg : . "is_bounded_default") :
theorem filter.limsup_le_limsup_of_le {α : Type u_1} {β : Type u_2} {f g : filter α} (h : f g) {u : α β} (hf : . "is_bounded_default") (hg : . "is_bounded_default") :
theorem filter.liminf_le_liminf_of_le {α : Type u_1} {β : Type u_2} {f g : filter α} (h : g f) {u : α β} (hf : . "is_bounded_default") (hg : . "is_bounded_default") :
theorem filter.Limsup_principal {α : Type u_1} {s : set α} (h : bdd_above s) (hs : s.nonempty) :
theorem filter.Liminf_principal {α : Type u_1} {s : set α} (h : bdd_below s) (hs : s.nonempty) :
theorem filter.limsup_congr {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α β} (h : ∀ᶠ (a : α) in f, u a = v a) :
=
theorem filter.blimsup_congr {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β α} {p : β Prop} (h : ∀ᶠ (a : β) in f, p a u a = v a) :
p = p
theorem filter.bliminf_congr {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β α} {p : β Prop} (h : ∀ᶠ (a : β) in f, p a u a = v a) :
p = p
theorem filter.liminf_congr {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α β} (h : ∀ᶠ (a : α) in f, u a = v a) :
=
theorem filter.limsup_const {β : Type u_2} {α : Type u_1} {f : filter α} [f.ne_bot] (b : β) :
filter.limsup (λ (x : α), b) f = b
theorem filter.liminf_const {β : Type u_2} {α : Type u_1} {f : filter α} [f.ne_bot] (b : β) :
filter.liminf (λ (x : α), b) f = b
@[simp]
theorem filter.Limsup_bot {α : Type u_1}  :
@[simp]
theorem filter.Liminf_bot {α : Type u_1}  :
@[simp]
theorem filter.Limsup_top {α : Type u_1}  :
@[simp]
theorem filter.Liminf_top {α : Type u_1}  :
@[simp]
theorem filter.blimsup_false {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
(λ (x : β), false) =
@[simp]
theorem filter.bliminf_false {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
(λ (x : β), false) =
theorem filter.limsup_const_bot {α : Type u_1} {β : Type u_2} {f : filter β} :
filter.limsup (λ (x : β), ) f =

Same as limsup_const applied to `⊥` but without the `ne_bot f` assumption

theorem filter.liminf_const_top {α : Type u_1} {β : Type u_2} {f : filter β} :
filter.liminf (λ (x : β), ) f =

Same as limsup_const applied to `⊤` but without the `ne_bot f` assumption

theorem filter.has_basis.Limsup_eq_infi_Sup {α : Type u_1} {ι : Sort u_2} {p : ι Prop} {s : ι set α} {f : filter α} (h : f.has_basis p s) :
f.Limsup = (i : ι) (hi : p i), has_Sup.Sup (s i)
theorem filter.has_basis.Liminf_eq_supr_Inf {α : Type u_1} {ι : Type u_4} {p : ι Prop} {s : ι set α} {f : filter α} (h : f.has_basis p s) :
f.Liminf = (i : ι) (hi : p i), has_Inf.Inf (s i)
theorem filter.Limsup_eq_infi_Sup {α : Type u_1} {f : filter α} :
f.Limsup = (s : set α) (H : s f),
theorem filter.Liminf_eq_supr_Inf {α : Type u_1} {f : filter α} :
f.Liminf = (s : set α) (H : s f),
theorem filter.limsup_le_supr {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
(n : β), u n
theorem filter.infi_le_liminf {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
( (n : β), u n)
theorem filter.limsup_eq_infi_supr {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
= (s : set β) (H : s f), (a : β) (H : a s), u a

In a complete lattice, the limsup of a function is the infimum over sets `s` in the filter of the supremum of the function over `s`

theorem filter.limsup_eq_infi_supr_of_nat {α : Type u_1} {u : α} :
= (n : ), (i : ) (H : i n), u i
theorem filter.limsup_eq_infi_supr_of_nat' {α : Type u_1} {u : α} :
= (n : ), (i : ), u (i + n)
theorem filter.has_basis.limsup_eq_infi_supr {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : ι Prop} {s : ι set β} {f : filter β} {u : β α} (h : f.has_basis p s) :
= (i : ι) (hi : p i), (a : β) (H : a s i), u a
theorem filter.blimsup_congr' {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} (h : ∀ᶠ (x : β) in f, u x (p x q x)) :
p = q
theorem filter.bliminf_congr' {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} (h : ∀ᶠ (x : β) in f, u x (p x q x)) :
p = q
theorem filter.blimsup_eq_infi_bsupr {α : Type u_1} {β : Type u_2} {f : filter β} {p : β Prop} {u : β α} :
p = (s : set β) (H : s f), (b : β) (hb : p b b s), u b
theorem filter.blimsup_eq_infi_bsupr_of_nat {α : Type u_1} {p : Prop} {u : α} :
= (i : ), (j : ) (hj : p j i j), u j
theorem filter.liminf_eq_supr_infi {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} :
= (s : set β) (H : s f), (a : β) (H : a s), u a

In a complete lattice, the liminf of a function is the infimum over sets `s` in the filter of the supremum of the function over `s`

theorem filter.liminf_eq_supr_infi_of_nat {α : Type u_1} {u : α} :
= (n : ), (i : ) (H : i n), u i
theorem filter.liminf_eq_supr_infi_of_nat' {α : Type u_1} {u : α} :
= (n : ), (i : ), u (i + n)
theorem filter.has_basis.liminf_eq_supr_infi {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : ι Prop} {s : ι set β} {f : filter β} {u : β α} (h : f.has_basis p s) :
= (i : ι) (hi : p i), (a : β) (H : a s i), u a
theorem filter.bliminf_eq_supr_binfi {α : Type u_1} {β : Type u_2} {f : filter β} {p : β Prop} {u : β α} :
p = (s : set β) (H : s f), (b : β) (hb : p b b s), u b
theorem filter.bliminf_eq_supr_binfi_of_nat {α : Type u_1} {p : Prop} {u : α} :
= (i : ), (j : ) (hj : p j i j), u j
theorem filter.limsup_eq_Inf_Sup {ι : Type u_1} {R : Type u_2} (F : filter ι) (a : ι R) :
= has_Inf.Inf ((λ (I : set ι), has_Sup.Sup (a '' I)) '' F.sets)
theorem filter.liminf_eq_Sup_Inf {ι : Type u_1} {R : Type u_2} (F : filter ι) (a : ι R) :
= has_Sup.Sup ((λ (I : set ι), has_Inf.Inf (a '' I)) '' F.sets)
@[simp]
theorem filter.liminf_nat_add {α : Type u_1} (f : α) (k : ) :
filter.liminf (λ (i : ), f (i + k)) filter.at_top =
@[simp]
theorem filter.limsup_nat_add {α : Type u_1} (f : α) (k : ) :
filter.limsup (λ (i : ), f (i + k)) filter.at_top =
theorem filter.liminf_le_of_frequently_le' {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {x : β} (h : ∃ᶠ (a : α) in f, u a x) :
x
theorem filter.le_limsup_of_frequently_le' {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {x : β} (h : ∃ᶠ (a : α) in f, x u a) :
x
@[simp]
theorem filter.complete_lattice_hom.apply_limsup_iterate {α : Type u_1} (f : α) (a : α) :

If `f : α → α` is a morphism of complete lattices, then the limsup of its iterates of any `a : α` is a fixed point.

theorem filter.complete_lattice_hom.apply_liminf_iterate {α : Type u_1} (f : α) (a : α) :

If `f : α → α` is a morphism of complete lattices, then the liminf of its iterates of any `a : α` is a fixed point.

theorem filter.blimsup_mono {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} (h : (x : β), p x q x) :
p q
theorem filter.bliminf_antitone {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} (h : (x : β), p x q x) :
q p
theorem filter.mono_blimsup' {α : Type u_1} {β : Type u_2} {f : filter β} {p : β Prop} {u v : β α} (h : ∀ᶠ (x : β) in f, p x u x v x) :
p p
theorem filter.mono_blimsup {α : Type u_1} {β : Type u_2} {f : filter β} {p : β Prop} {u v : β α} (h : (x : β), p x u x v x) :
p p
theorem filter.mono_bliminf' {α : Type u_1} {β : Type u_2} {f : filter β} {p : β Prop} {u v : β α} (h : ∀ᶠ (x : β) in f, p x u x v x) :
p p
theorem filter.mono_bliminf {α : Type u_1} {β : Type u_2} {f : filter β} {p : β Prop} {u v : β α} (h : (x : β), p x u x v x) :
p p
theorem filter.bliminf_antitone_filter {α : Type u_1} {β : Type u_2} {f g : filter β} {p : β Prop} {u : β α} (h : f g) :
p p
theorem filter.blimsup_monotone_filter {α : Type u_1} {β : Type u_2} {f g : filter β} {p : β Prop} {u : β α} (h : f g) :
p p
@[simp]
theorem filter.blimsup_and_le_inf {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} :
(λ (x : β), p x q x) p q
@[simp]
theorem filter.bliminf_sup_le_and {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} :
p q (λ (x : β), p x q x)
@[simp]
theorem filter.blimsup_sup_le_or {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} :
p q (λ (x : β), p x q x)

See also `filter.blimsup_or_eq_sup`.

@[simp]
theorem filter.bliminf_or_le_inf {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} :
(λ (x : β), p x q x) p q

See also `filter.bliminf_or_eq_inf`.

theorem filter.order_iso.apply_blimsup {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter β} {p : β Prop} {u : β α} (e : α ≃o γ) :
e f p) = filter.blimsup (e u) f p
theorem filter.order_iso.apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter β} {p : β Prop} {u : β α} (e : α ≃o γ) :
e f p) = filter.bliminf (e u) f p
theorem filter.Sup_hom.apply_blimsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter β} {p : β Prop} {u : β α} (g : γ) :
g f p) filter.blimsup (g u) f p
theorem filter.Inf_hom.le_apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter β} {p : β Prop} {u : β α} (g : γ) :
filter.bliminf (g u) f p g f p)
@[simp]
theorem filter.blimsup_or_eq_sup {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} :
(λ (x : β), p x q x) = p q
@[simp]
theorem filter.bliminf_or_eq_inf {α : Type u_1} {β : Type u_2} {f : filter β} {p q : β Prop} {u : β α} :
(λ (x : β), p x q x) = p q
theorem filter.sup_limsup {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} [f.ne_bot] (a : α) :
a = filter.limsup (λ (x : β), a u x) f
theorem filter.inf_liminf {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} [f.ne_bot] (a : α) :
a = filter.liminf (λ (x : β), a u x) f
theorem filter.sup_liminf {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} (a : α) :
a = filter.liminf (λ (x : β), a u x) f
theorem filter.inf_limsup {α : Type u_1} {β : Type u_2} {f : filter β} {u : β α} (a : α) :
a = filter.limsup (λ (x : β), a u x) f
theorem filter.limsup_compl {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) :
f) =
theorem filter.liminf_compl {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) :
f) =
theorem filter.limsup_sdiff {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) (a : α) :
\ a = filter.limsup (λ (b : β), u b \ a) f
theorem filter.liminf_sdiff {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) [f.ne_bot] (a : α) :
\ a = filter.liminf (λ (b : β), u b \ a) f
theorem filter.sdiff_limsup {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) [f.ne_bot] (a : α) :
a \ = filter.liminf (λ (b : β), a \ u b) f
theorem filter.sdiff_liminf {α : Type u_1} {β : Type u_2} (f : filter β) (u : β α) (a : α) :
a \ = filter.limsup (λ (b : β), a \ u b) f
theorem filter.cofinite.blimsup_set_eq {α : Type u_1} {ι : Type u_4} {p : ι Prop} {s : ι set α} :
= {x : α | {n : ι | p n x s n}.infinite}
theorem filter.cofinite.bliminf_set_eq {α : Type u_1} {ι : Type u_4} {p : ι Prop} {s : ι set α} :
= {x : α | {n : ι | p n x s n}.finite}
theorem filter.cofinite.limsup_set_eq {α : Type u_1} {ι : Type u_4} {s : ι set α} :
= {x : α | {n : ι | x s n}.infinite}

In other words, `limsup cofinite s` is the set of elements lying inside the family `s` infinitely often.

theorem filter.cofinite.liminf_set_eq {α : Type u_1} {ι : Type u_4} {s : ι set α} :
= {x : α | {n : ι | x s n}.finite}

In other words, `liminf cofinite s` is the set of elements lying outside the family `s` finitely often.

theorem filter.exists_forall_mem_of_has_basis_mem_blimsup {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : filter β} {b : ι set β} {q : ι Prop} (hl : l.has_basis q b) {u : β set α} {p : β Prop} {x : α} (hx : x p) :
(f : {i : ι | q i} β), (i : {i : ι | q i}), x u (f i) p (f i) f i b i
theorem filter.exists_forall_mem_of_has_basis_mem_blimsup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : filter β} {b : ι set β} (hl : l.has_basis (λ (_x : ι), true) b) {u : β set α} {p : β Prop} {x : α} (hx : x p) :
(f : ι β), (i : ι), x u (f i) p (f i) f i b i
theorem filter.frequently_lt_of_lt_Limsup {α : Type u_1} {f : filter α} {a : α} (hf : . "is_bounded_default") (h : a < f.Limsup) :
∃ᶠ (n : α) in f, a < n
theorem filter.frequently_lt_of_Liminf_lt {α : Type u_1} {f : filter α} {a : α} (hf : . "is_bounded_default") (h : f.Liminf < a) :
∃ᶠ (n : α) in f, n < a
theorem filter.eventually_lt_of_lt_liminf {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {b : β} (h : b < ) (hu : . "is_bounded_default") :
∀ᶠ (a : α) in f, b < u a
theorem filter.eventually_lt_of_limsup_lt {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {b : β} (h : < b) (hu : . "is_bounded_default") :
∀ᶠ (a : α) in f, u a < b
theorem filter.le_limsup_of_frequently_le {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {b : β} (hu_le : ∃ᶠ (x : α) in f, b u x) (hu : . "is_bounded_default") :
b
theorem filter.liminf_le_of_frequently_le {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {b : β} (hu_le : ∃ᶠ (x : α) in f, u x b) (hu : . "is_bounded_default") :
b
theorem filter.frequently_lt_of_lt_limsup {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {b : β} (hu : . "is_bounded_default") (h : b < ) :
∃ᶠ (x : α) in f, b < u x
theorem filter.frequently_lt_of_liminf_lt {α : Type u_1} {β : Type u_2} {f : filter α} {u : α β} {b : β} (hu : . "is_bounded_default") (h : < b) :
∃ᶠ (x : α) in f, u x < b
theorem filter.lt_mem_sets_of_Limsup_lt {α : Type u_1} {f : filter α} {b : α} (h : f) (l : f.Limsup < b) :
∀ᶠ (a : α) in f, a < b
theorem filter.gt_mem_sets_of_Liminf_gt {α : Type u_1} {f : filter α} {b : α} :
b < f.Liminf (∀ᶠ (a : α) in f, b < a)
theorem monotone.is_bounded_under_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [nonempty β] [linear_order β] [preorder γ] [no_max_order γ] {g : β γ} {f : α β} {l : filter α} (hg : monotone g) (hg' : filter.at_top) :
theorem monotone.is_bounded_under_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [nonempty β] [linear_order β] [preorder γ] [no_min_order γ] {g : β γ} {f : α β} {l : filter α} (hg : monotone g) (hg' : filter.at_bot) :
(g f)
theorem antitone.is_bounded_under_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [nonempty β] [linear_order β] [preorder γ] [no_max_order γ] {g : β γ} {f : α β} {l : filter α} (hg : antitone g) (hg' : filter.at_top) :
(g f)
theorem antitone.is_bounded_under_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [nonempty β] [linear_order β] [preorder γ] [no_min_order γ] {g : β γ} {f : α β} {l : filter α} (hg : antitone g) (hg' : filter.at_bot) :
(g f)
theorem galois_connection.l_limsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {v : α β} {l : β γ} {u : γ β} (gc : u) (hlv : (λ (x : α), l (v x)) . "is_bounded_default") (hv_co : . "is_bounded_default") :
l f) filter.limsup (λ (x : α), l (v x)) f
theorem order_iso.limsup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {u : α β} (g : β ≃o γ) (hu : . "is_bounded_default") (hu_co : . "is_bounded_default") (hgu : (λ (x : α), g (u x)) . "is_bounded_default") (hgu_co : (λ (x : α), g (u x)) . "is_bounded_default") :
g f) = filter.limsup (λ (x : α), g (u x)) f
theorem order_iso.liminf_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : filter α} {u : α β} (g : β ≃o γ) (hu : . "is_bounded_default") (hu_co : . "is_bounded_default") (hgu : (λ (x : α), g (u x)) . "is_bounded_default") (hgu_co : (λ (x : α), g (u x)) . "is_bounded_default") :
g f) = filter.liminf (λ (x : α), g (u x)) f