case h.e'_3.h.e'_4
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
t : Set α
ht : Set.Finite t
⊢ t = ↑(Finite.toFinset ht)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
t : Set α
ht : Set.Finite t
⊢ Dense (s \ t)
convert hs.diff_finset ht.toFinset
no goals
case h.e'_3.h.e'_4
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
t : Set α
ht : Set.Finite t
⊢ t = ↑(Finite.toFinset ht)
exact (Finite.coe_toFinset _).symm