Theorems · Theorem · general topology

HasCountableSeparatingOn.exists_countable_separating

∀ {α : Type u_1} {p : Set α → Prop} {t : Set α} [self : 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

5 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

HasCountableSeparatingOn