Theorems · Theorem · general topology

Filter.IsBoundedUnder.isCoboundedUnder_ge

∀ {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [inst : Preorder α] [l.NeBot],
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) l u

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

6 results in Mathlib

Foundations

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

Assumes

PreorderFilter.NeBot