Theorems · Theorem · general topology

Antitone.isCoboundedUnder_ge_of_isCobounded

∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Antitone f →
    ∀ [F.NeBot], Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) F f

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderLinearOrderFilter.NeBot