# Lemmas about `Is(Co)Bounded(Under)` #

This file proves several lemmas about `IsBounded`, `IsBoundedUnder`, `IsCobounded` and `IsCoboundedUnder`.

source
theorem Filter.isBounded_iff {α : Type u_1} {r : α → α → Prop} {f : Filter α} :
IsBounded r f ↔ ∃ 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.

source
theorem Filter.isBoundedUnder_of {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter β} {u : β → α} :
(∃ (b : α), ∀ (x : β), r (u x) b) → IsBoundedUnder r f u

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

source
theorem Filter.isBounded_bot {α : Type u_1} {r : α → α → Prop} :
IsBounded r ⊥ ↔ Nonempty α
source
theorem Filter.isBounded_top {α : Type u_1} {r : α → α → Prop} :
IsBounded r ⊤ ↔ ∃ (t : α), ∀ (x : α), r x t
source
theorem Filter.isBounded_principal {α : Type u_1} {r : α → α → Prop} (s : Set α) :
IsBounded r (principal s) ↔ ∃ (t : α), ∀ x ∈ s, r x t
source
theorem Filter.isBounded_sup {α : Type u_1} {r : α → α → Prop} {f g : Filter α} [IsTrans α r] [IsDirected α r] :
IsBounded r f → IsBounded r g → IsBounded r (f ⊔ g)
source
theorem Filter.IsBounded.mono {α : Type u_1} {r : α → α → Prop} {f g : Filter α} (h : f ≤ g) :
IsBounded r g → IsBounded r f
source
theorem Filter.IsBoundedUnder.mono {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f g : Filter β} {u : β → α} (h : f ≤ g) :
IsBoundedUnder r g u → IsBoundedUnder r f u
source
theorem Filter.IsBoundedUnder.mono_le {α : Type u_1} {β : Type u_2} [Preorder β] {l : Filter α} {u v : α → β} (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l u) (hv : v ≤ᶠ[l] u) :
IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l v
source
theorem Filter.IsBoundedUnder.mono_ge {α : Type u_1} {β : Type u_2} [Preorder β] {l : Filter α} {u v : α → β} (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l u) (hv : u ≤ᶠ[l] v) :
IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l v
source
theorem Filter.isBoundedUnder_const {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [IsRefl α r] {l : Filter β} {a : α} :
IsBoundedUnder r l fun (x : β) => a
source
theorem Filter.IsBounded.isBoundedUnder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter α} {q : β → β → Prop} {u : α → β} (hu : ∀ (a₀ a₁ : α), r a₀ a₁ → q (u a₀) (u a₁)) :
IsBounded r f → IsBoundedUnder q f u
source
theorem Filter.IsBoundedUnder.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {l : Filter γ} {q : β → β → Prop} {u : γ → α} {v : α → β} (hv : ∀ (a₀ a₁ : α), r a₀ a₁ → q (v a₀) (v a₁)) :
IsBoundedUnder r l u → IsBoundedUnder q l (v ∘ u)
source
theorem Filter.isBoundedUnder_map_iff {ι : Type u_5} {κ : Type u_6} {X : Type u_7} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter κ} :
IsBoundedUnder r (map φ 𝓕) f ↔ IsBoundedUnder r 𝓕 (f ∘ φ)
source
theorem Filter.Tendsto.isBoundedUnder_comp {ι : Type u_5} {κ : Type u_6} {X : Type u_7} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter ι} {𝓖 : Filter κ} (φ_tendsto : Tendsto φ 𝓖 𝓕) (𝓕_bounded : IsBoundedUnder r 𝓕 f) :
IsBoundedUnder r 𝓖 (f ∘ φ)
source
theorem Filter.IsBoundedUnder.eventually_le {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (h : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) :
∃ (a : α), ∀ᶠ (x : β) in f, u x ≤ a
source
theorem Filter.IsBoundedUnder.eventually_ge {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (h : IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) :
∃ (a : α), ∀ᶠ (x : β) in f, a ≤ u x
source
theorem Filter.isBoundedUnder_of_eventually_le {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {a : α} (h : ∀ᶠ (x : β) in f, u x ≤ a) :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
source
theorem Filter.isBoundedUnder_of_eventually_ge {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {a : α} (h : ∀ᶠ (x : β) in f, a ≤ u x) :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
source
theorem Filter.isBoundedUnder_iff_eventually_bddAbove {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ↔ ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
source
theorem Filter.isBoundedUnder_iff_eventually_bddBelow {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u ↔ ∃ (s : Set β), BddBelow (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
source
theorem BddAbove.isBoundedUnder {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {s : Set β} (hs : s ∈ f) (hu : BddAbove (u '' s)) :
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
source
theorem BddAbove.isBoundedUnder_of_range {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (hu : BddAbove (Set.range u)) :
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

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

source
theorem BddBelow.isBoundedUnder {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {s : Set β} (hs : s ∈ f) (hu : BddBelow (u '' s)) :
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
source
theorem BddBelow.isBoundedUnder_of_range {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (hu : BddBelow (Set.range u)) :
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

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

source
theorem Filter.IsBoundedUnder.le_of_finite {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Finite β] {f : Filter β} {u : β → α} :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
source
theorem Filter.IsBoundedUnder.ge_of_finite {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Finite β] {f : Filter β} {u : β → α} :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
source
theorem Monotone.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Monotone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l (v ∘ u)
source
theorem Monotone.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Monotone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l (v ∘ u)
source
theorem Antitone.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l (v ∘ u)
source
theorem Antitone.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l (v ∘ u)
source
theorem Filter.not_isBoundedUnder_of_tendsto_atTop {α : Type u_1} {β : Type u_2} [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α} [l.NeBot] (hf : Tendsto f l atTop) :
¬IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f
source
theorem Filter.not_isBoundedUnder_of_tendsto_atBot {α : Type u_1} {β : Type u_2} [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α} [l.NeBot] (hf : Tendsto f l atBot) :
¬IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f
source
theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite {α : Type u_1} {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {f : α → β} (hf : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) cofinite f) :
BddAbove (Set.range f)
source
theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite {α : Type u_1} {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] {f : α → β} (hf : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) cofinite f) :
BddBelow (Set.range f)
source
theorem Filter.IsBoundedUnder.bddAbove_range {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {f : ℕ → β} (hf : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) atTop f) :
BddAbove (Set.range f)
source
theorem Filter.IsBoundedUnder.bddBelow_range {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] {f : ℕ → β} (hf : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) atTop f) :
BddBelow (Set.range f)
source
theorem Filter.IsCobounded.mk {α : Type u_1} {r : α → α → Prop} {f : Filter α} [IsTrans α r] (a : α) (h : ∀ s ∈ f, ∃ x ∈ s, r a x) :
IsCobounded r f

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.

source
theorem Filter.IsBounded.isCobounded_flip {α : Type u_1} {r : α → α → Prop} {f : Filter α} [IsTrans α r] [f.NeBot] :
IsBounded r f → IsCobounded (flip r) f

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

source
theorem Filter.IsBounded.isCobounded_ge {α : Type u_1} {f : Filter α} [Preorder α] [f.NeBot] (h : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f) :
IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f
source
theorem Filter.IsBounded.isCobounded_le {α : Type u_1} {f : Filter α} [Preorder α] [f.NeBot] (h : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f) :
IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f
source
theorem Filter.IsBoundedUnder.isCoboundedUnder_flip {α : Type u_1} {γ : Type u_3} {r : α → α → Prop} {u : γ → α} {l : Filter γ} [IsTrans α r] [l.NeBot] (h : IsBoundedUnder r l u) :
IsCoboundedUnder (flip r) l u
source
theorem Filter.IsBoundedUnder.isCoboundedUnder_le {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [Preorder α] [l.NeBot] (h : IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
source
theorem Filter.IsBoundedUnder.isCoboundedUnder_ge {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [Preorder α] [l.NeBot] (h : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
source
theorem Filter.isCoboundedUnder_le_of_eventually_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ᶠ (i : ι) in l, x ≤ f i) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f
source
theorem Filter.isCoboundedUnder_ge_of_eventually_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ᶠ (i : ι) in l, f i ≤ x) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l f
source
theorem Filter.isCoboundedUnder_le_of_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ (i : ι), x ≤ f i) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f
source
theorem Filter.isCoboundedUnder_ge_of_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ (i : ι), f i ≤ x) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l f
source
theorem Filter.isCobounded_bot {α : Type u_1} {r : α → α → Prop} :
IsCobounded r ⊥ ↔ ∃ (b : α), ∀ (x : α), r b x
source
theorem Filter.isCobounded_top {α : Type u_1} {r : α → α → Prop} :
IsCobounded r ⊤ ↔ Nonempty α
source
theorem Filter.isCobounded_principal {α : Type u_1} {r : α → α → Prop} (s : Set α) :
IsCobounded r (principal s) ↔ ∃ (b : α), ∀ (a : α), (∀ x ∈ s, r x a) → r b a
source
theorem Filter.IsCobounded.mono {α : Type u_1} {r : α → α → Prop} {f g : Filter α} (h : f ≤ g) :
IsCobounded r f → IsCobounded r g
source
theorem Filter.IsCobounded.frequently_ge {α : Type u_1} {f : Filter α} [LinearOrder α] [f.NeBot] (cobdd : IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f) :
∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness from below.

source
theorem Filter.IsCobounded.frequently_le {α : Type u_1} {f : Filter α} [LinearOrder α] [f.NeBot] (cobdd : IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f) :
∃ (u : α), ∃ᶠ (x : α) in f, x ≤ u

For nontrivial filters in linear orders, coboundedness for `≥` implies frequent boundedness from above.

source
theorem Filter.IsCobounded.of_frequently_ge {α : Type u_1} {f : Filter α} [LinearOrder α] {l : α} (freq_ge : ∃ᶠ (x : α) in f, l ≤ x) :
IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f

In linear orders, frequent boundedness from below implies coboundedness for `≤`.

source
theorem Filter.IsCobounded.of_frequently_le {α : Type u_1} {f : Filter α} [LinearOrder α] {u : α} (freq_le : ∃ᶠ (r : α) in f, r ≤ u) :
IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f

In linear orders, frequent boundedness from above implies coboundedness for `≥`.

source
theorem Filter.IsCoboundedUnder.frequently_ge {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α} (h : IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) :
∃ (a : α), ∃ᶠ (x : ι) in f, a ≤ u x
source
theorem Filter.IsCoboundedUnder.frequently_le {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α} (h : IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) :
∃ (a : α), ∃ᶠ (x : ι) in f, u x ≤ a
source
theorem Filter.IsCoboundedUnder.of_frequently_ge {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_ge : ∃ᶠ (x : ι) in f, a ≤ u x) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
source
theorem Filter.IsCoboundedUnder.of_frequently_le {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_le : ∃ᶠ (x : ι) in f, u x ≤ a) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
source
theorem Filter.isBoundedUnder_sum {α : Type u_5} {f : Filter α} {R : Type u_6} {κ : Type u_7} [AddCommMonoid R] {r : R → R → Prop} (hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)) (hr₀ : r 0 0) {u : κ → α → R} (s : Finset κ) (h : ∀ k ∈ s, IsBoundedUnder r f (u k)) :
IsBoundedUnder r f (∑ k ∈ s, u k)
source
theorem Filter.isBoundedUnder_ge_add {α : Type u_5} {f : Filter α} {R : Type u_6} [Preorder R] [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R} (u_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f u) (v_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f v) :
IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u + v)
source
theorem Filter.isBoundedUnder_le_add {α : Type u_5} {f : Filter α} {R : Type u_6} [Preorder R] [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R} (u_bdd_le : IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f u) (v_bdd_le : IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f v) :
IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u + v)
source
theorem Filter.isBoundedUnder_le_sum {α : Type u_5} {f : Filter α} {R : Type u_6} [Preorder R] {κ : Type u_7} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ) :
(∀ k ∈ s, IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u k)) → IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (∑ k ∈ s, u k)
source
theorem Filter.isBoundedUnder_ge_sum {α : Type u_5} {f : Filter α} {R : Type u_6} [Preorder R] {κ : Type u_7} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ) :
(∀ k ∈ s, IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u k)) → IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (∑ k ∈ s, u k)
source
theorem Filter.isCoboundedUnder_ge_add {α : Type u_5} {R : Type u_6} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot] [AddLeftMono R] [AddRightMono R] {u v : α → R} (hu : IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f u) (hv : IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f v) :
IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u + v)
source
theorem Filter.isCoboundedUnder_le_add {α : Type u_5} {R : Type u_6} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot] [AddLeftMono R] [AddRightMono R] {u v : α → R} (hu : IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f u) (hv : IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f v) :
IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u + v)
source
theorem Filter.isBoundedUnder_le_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [Preorder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v) :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f (u * v)
source
theorem Filter.isCoboundedUnder_ge_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [LinearOrder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v) :
IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f (u * v)
source
theorem Filter.isBounded_le_atBot {α : Type u_1} [Preorder α] [Nonempty α] :
IsBounded (fun (x1 x2 : α) => x1 ≤ x2) atBot
source
theorem Filter.isBounded_ge_atTop {α : Type u_1} [Preorder α] [Nonempty α] :
IsBounded (fun (x1 x2 : α) => x1 ≥ x2) atTop
source
theorem Filter.Tendsto.isBoundedUnder_le_atBot {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] {f : Filter β} {u : β → α} (h : Tendsto u f atBot) :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
source
theorem Filter.Tendsto.isBoundedUnder_ge_atTop {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] {f : Filter β} {u : β → α} (h : Tendsto u f atTop) :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
source
theorem Filter.bddAbove_range_of_tendsto_atTop_atBot {α : Type u_1} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {u : ℕ → α} (hx : Tendsto u atTop atBot) :
BddAbove (Set.range u)
source
theorem Filter.bddBelow_range_of_tendsto_atTop_atTop {α : Type u_1} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {u : ℕ → α} (hx : Tendsto u atTop atTop) :
BddBelow (Set.range u)
source
theorem Filter.isCobounded_le_of_bot {α : Type u_1} [LE α] [OrderBot α] {f : Filter α} :
IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f
source
theorem Filter.isCobounded_ge_of_top {α : Type u_1} [LE α] [OrderTop α] {f : Filter α} :
IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f
source
theorem Filter.isBounded_le_of_top {α : Type u_1} [LE α] [OrderTop α] {f : Filter α} :
IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f
source
theorem Filter.isBounded_ge_of_bot {α : Type u_1} [LE α] [OrderBot α] {f : Filter α} :
IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f
source
@[simp]
theorem OrderIso.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :
(Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l fun (x : γ) => e (u x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
source
@[simp]
theorem OrderIso.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :
(Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l fun (x : γ) => e (u x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
source
@[simp]
theorem Filter.isBoundedUnder_le_inv {α : Type u_1} {β : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {l : Filter β} {u : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => (u x)⁻¹) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
source
@[simp]
theorem Filter.isBoundedUnder_le_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {l : Filter β} {u : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => -u x) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
source
@[simp]
theorem Filter.isBoundedUnder_ge_inv {α : Type u_1} {β : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {l : Filter β} {u : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => (u x)⁻¹) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
source
@[simp]
theorem Filter.isBoundedUnder_ge_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {l : Filter β} {u : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => -u x) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
source
theorem Filter.IsBoundedUnder.sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {f : Filter β} {u v : β → α} :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u → IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v → IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => u a ⊔ v a
source
@[simp]
theorem Filter.isBoundedUnder_le_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {f : Filter β} {u v : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => u a ⊔ v a) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ∧ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v
source
theorem Filter.IsBoundedUnder.inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] {f : Filter β} {u v : β → α} :
IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u → IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v → IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f fun (a : β) => u a ⊓ v a
source
@[simp]
theorem Filter.isBoundedUnder_ge_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] {f : Filter β} {u v : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f fun (a : β) => u a ⊓ v a) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u ∧ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v
source
theorem Filter.isBoundedUnder_le_abs {α : Type u_1} {β : Type u_2} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {f : Filter β} {u : β → α} :
(IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => |u a|) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ∧ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
source
def Filter.tacticIsBoundedDefault :
Lean.ParserDescr

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 `isBoundedDefault` in the statements, in the form `(hf : f.IsBounded (≥) := by isBoundedDefault)`.

Equations

- Filter.tacticIsBoundedDefault = Lean.ParserDescr.node `Filter.tacticIsBoundedDefault 1024 (Lean.ParserDescr.nonReservedSymbol "isBoundedDefault" false)

Instances For

source
theorem Monotone.isBoundedUnder_le_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Filter.Tendsto g Filter.atTop Filter.atTop) :
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f
source
theorem Monotone.isBoundedUnder_ge_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Filter.Tendsto g Filter.atBot Filter.atBot) :
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f
source
theorem Antitone.isBoundedUnder_le_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Filter.Tendsto g Filter.atBot Filter.atTop) :
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f
source
theorem Antitone.isBoundedUnder_ge_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Filter.Tendsto g Filter.atTop Filter.atBot) :
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f
source
theorem isCoboundedUnder_le_max {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : Filter α} {u v : α → β} (h : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u ∨ Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v) :
Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => max (u a) (v a)
source
theorem isBoundedUnder_le_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup' hs fun (i : ι) => F i a
source
theorem isCoboundedUnder_le_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) :
Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup' hs fun (i : ι) => F i a
source
theorem isBoundedUnder_le_finset_sup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup fun (i : ι) => F i a
source
theorem isBoundedUnder_ge_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf' hs fun (i : ι) => F i a
source
theorem isCoboundedUnder_ge_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) :
Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf' hs fun (i : ι) => F i a
source
theorem isBoundedUnder_ge_finset_inf {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) :
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf fun (i : ι) => F i a
source
theorem Monotone.frequently_ge_map_of_frequently_ge {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) {l : R} (freq_ge : ∃ᶠ (x : R) in F, l ≤ x) :
∃ᶠ (x' : S) in Filter.map f F, f l ≤ x'
source
theorem Monotone.frequently_le_map_of_frequently_le {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) {u : R} (freq_le : ∃ᶠ (x : R) in F, x ≤ u) :
∃ᶠ (y : S) in Filter.map f F, y ≤ f u
source
theorem Antitone.frequently_le_map_of_frequently_ge {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) {l : R} (frbdd : ∃ᶠ (x : R) in F, l ≤ x) :
∃ᶠ (y : S) in Filter.map f F, y ≤ f l
source
theorem Antitone.frequently_ge_map_of_frequently_le {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) {u : R} (frbdd : ∃ᶠ (x : R) in F, x ≤ u) :
∃ᶠ (y : S) in Filter.map f F, f u ≤ y
source
theorem Monotone.isCoboundedUnder_le_of_isCobounded {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F) :
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≤ x2) F f
source
theorem Monotone.isCoboundedUnder_ge_of_isCobounded {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F) :
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≥ x2) F f
source
theorem Antitone.isCoboundedUnder_le_of_isCobounded {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F) :
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≤ x2) F f
source
theorem Antitone.isCoboundedUnder_ge_of_isCobounded {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F) :
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≥ x2) F f