Lemmas about Is(Co)Bounded(Under)

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

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.

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.

theorem Filter.isBounded_bot {α : Type u_1} {r : α → α → Prop} : IsBounded r ⊥ ↔ Nonempty α

theorem Filter.isBounded_top {α : Type u_1} {r : α → α → Prop} : IsBounded r ⊤ ↔ ∃ (t : α), ∀ (x : α), r x t

theorem Filter.isBounded_principal {α : Type u_1} {r : α → α → Prop} (s : Set α) : IsBounded r (principal s) ↔ ∃ (t : α), ∀ x ∈ s, r x t

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)

theorem Filter.IsBounded.mono {α : Type u_1} {r : α → α → Prop} {f g : Filter α} (h : f ≤ g) : IsBounded r g → IsBounded r f

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

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

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

theorem Filter.isBoundedUnder_const {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [IsRefl α r] {l : Filter β} {a : α} : IsBoundedUnder r l fun (x : β) => a

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

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)

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 ∘ φ)

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 ∘ φ)

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

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

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

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

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

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

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

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.

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

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.

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

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

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)

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)

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)

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)

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

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

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)

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)

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)

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)

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.

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.

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

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

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

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

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

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

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

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

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

theorem Filter.isCobounded_bot {α : Type u_1} {r : α → α → Prop} : IsCobounded r ⊥ ↔ ∃ (b : α), ∀ (x : α), r b x

theorem Filter.isCobounded_top {α : Type u_1} {r : α → α → Prop} : IsCobounded r ⊤ ↔ Nonempty α

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

theorem Filter.IsCobounded.mono {α : Type u_1} {r : α → α → Prop} {f g : Filter α} (h : f ≤ g) : IsCobounded r f → IsCobounded r g

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.

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.

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 ≤.

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 ≥.

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

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

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

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

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)

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)

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)

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)

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)

theorem Filter.isCoboundedUnder_ge_add {α : Type u_5} {R : Type u_6} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot] [CovariantClass R R (fun (a b : R) => a + b) fun (x1 x2 : R) => x1 ≤ x2] [CovariantClass R R (fun (a b : R) => b + a) fun (x1 x2 : R) => x1 ≤ x2] {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)

theorem Filter.isCoboundedUnder_le_add {α : Type u_5} {R : Type u_6} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot] [CovariantClass R R (fun (a b : R) => a + b) fun (x1 x2 : R) => x1 ≤ x2] [CovariantClass R R (fun (a b : R) => b + a) fun (x1 x2 : R) => x1 ≤ x2] {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)

theorem Filter.isBoundedUnder_le_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u) (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)

theorem Filter.isCoboundedUnder_ge_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [Mul α] [Zero α] [LinearOrder α] [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)

theorem Filter.isBounded_le_atBot {α : Type u_1} [Preorder α] [Nonempty α] : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) atBot

theorem Filter.isBounded_ge_atTop {α : Type u_1} [Preorder α] [Nonempty α] : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) atTop

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

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

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)

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)

theorem Filter.isCobounded_le_of_bot {α : Type u_1} [LE α] [OrderBot α] {f : Filter α} : IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f

theorem Filter.isCobounded_ge_of_top {α : Type u_1} [LE α] [OrderTop α] {f : Filter α} : IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f

theorem Filter.isBounded_le_of_top {α : Type u_1} [LE α] [OrderTop α] {f : Filter α} : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f

theorem Filter.isBounded_ge_of_bot {α : Type u_1} [LE α] [OrderBot α] {f : Filter α} : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f

@[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

@[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

@[simp]

theorem Filter.isBoundedUnder_le_inv {α : Type u_1} {β : Type u_2} [OrderedCommGroup α] {l : Filter β} {u : β → α} : (IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => (u x)⁻¹) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u

@[simp]

theorem Filter.isBoundedUnder_le_neg {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup α] {l : Filter β} {u : β → α} : (IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => -u x) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u

@[simp]

theorem Filter.isBoundedUnder_ge_inv {α : Type u_1} {β : Type u_2} [OrderedCommGroup α] {l : Filter β} {u : β → α} : (IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => (u x)⁻¹) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u

@[simp]

theorem Filter.isBoundedUnder_ge_neg {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup α] {l : Filter β} {u : β → α} : (IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => -u x) ↔ IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u

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

@[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

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

@[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

theorem Filter.isBoundedUnder_le_abs {α : Type u_1} {β : Type u_2} [LinearOrderedAddCommGroup α] {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

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)

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

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

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

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

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 : α) => u a ⊔ v a

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

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

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

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

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

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

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'

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

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

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

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

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

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

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