simp
case h.e'_2.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T2Space E
s t x✝ : Finset E
⊢ x✝ ∈ {t | t ⊆ s} ↔ x✝ ∈ ↑s.powerset
no goals