Theorems · Theorem · general topology

HasCountableSeparatingOn.of_subtype

∀ {α : Type u_1} {p : Set α → Prop} {t : Set α} {q : Set ↑t → Prop} [h : HasCountableSeparatingOn (↑t) q Set.univ],
  (∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U) → HasCountableSeparatingOn α p t

Defined in

Mathlib.Order.Filter.CountableSeparatingOn

Cited by

1 results in Mathlib

Foundations

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

Assumes

HasCountableSeparatingOn