Theorems · Theorem · general topology

Filter.exists_singleton_mem_of_forall_separating

∀ {α : Type u_1} {l : Filter α} [CountableInterFilter l] [Nonempty α] (p : Set α → Prop)
  [HasCountableSeparatingOn α p Set.univ], (∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) → ∃ x, {x} ∈ l

Defined in

Mathlib.Order.Filter.CountableSeparatingOn

Cited by

1 results in Mathlib

Foundations

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

Assumes

CountableInterFilterNonemptyHasCountableSeparatingOn