Theorems · Theorem · general topology

Antitone.frequently_le_map_of_frequently_ge

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

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderLinearOrder