Theorems · Theorem · general topology

Monotone.frequently_le_map_of_frequently_le

∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Monotone f → ∀ {l : R}, (∃ᶠ (x : R) in F, x ≤ l) → ∃ᶠ (x' : S) in Filter.map f F, x' ≤ f l

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

2 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderLinearOrder