Theorems · Theorem · general topology

exists_nonempty_countable_separating

∀ (α : Type u_1) {p : Set α → Prop} {s₀ : Set α},
  p s₀ →
    ∀ (t : Set α) [HasCountableSeparatingOn α p t],
      ∃ S, S.Nonempty ∧ S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Defined in

Mathlib.Order.Filter.CountableSeparatingOn

Cited by

1 results in Mathlib

Foundations

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

Assumes

HasCountableSeparatingOn