[GOAL]
X : Type ?u.7
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
⊢ HasCountableSeparatingOn X IsOpen s
[PROOFSTEP]
suffices HasCountableSeparatingOn s IsOpen univ from .of_subtype fun _ ↦ isOpen_induced_iff.1
[GOAL]
X : Type ?u.7
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
⊢ HasCountableSeparatingOn (↑s) IsOpen univ
[PROOFSTEP]
refine ⟨⟨countableBasis s, countable_countableBasis _, fun _ ↦ isOpen_of_mem_countableBasis, fun x _ y _ h ↦ ?_⟩⟩
[GOAL]
X : Type ?u.7
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
x : ↑s
x✝¹ : x ∈ univ
y : ↑s
x✝ : y ∈ univ
h : ∀ (s_1 : Set ↑s), s_1 ∈ countableBasis ↑s → (x ∈ s_1 ↔ y ∈ s_1)
⊢ x = y
[PROOFSTEP]
exact ((isBasis_countableBasis _).inseparable_iff.2 h).eq
