Theorems · Theorem · general topology

exists_countable_separating

∀ (α : Type u_1) (p : Set α → Prop) (t : Set α) [h : HasCountableSeparatingOn α p t],
  ∃ S, 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 7 from the axioms · uses no axioms

Assumes

HasCountableSeparatingOn