Theorems · Theorem · general topology

Monotone.isBoundedUnder_le_comp_iff

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [inst : LinearOrder β] [inst_1 : Preorder γ] [NoMaxOrder γ]
  {g : β → γ} {f : α → β} {l : Filter α},
  Monotone g →
    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)

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

2 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonemptyLinearOrderPreorderNoMaxOrder