Theorems · Theorem · general topology

Filter.forall_neBot_le_iff

∀ {α : Type u} {g : Filter α} {p : Filter α → Prop},
  Monotone p → ((∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f)

Defined in

Mathlib.Order.Filter.Ultrafilter.Defs

Cited by

1 results in Mathlib

Foundations

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