α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s ⊆ {a | 𝓝 a ≤ 𝓟 s} ↔ ∀ (a : α), a ∈ s → 𝓝 a ≤ 𝓟 s
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s ⊆ interior s ↔ ∀ (a : α), a ∈ s → 𝓝 a ≤ 𝓟 s
rw [interior_eq_nhds]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s ⊆ {a | 𝓝 a ≤ 𝓟 s} ↔ ∀ (a : α), a ∈ s → 𝓝 a ≤ 𝓟 s
rfl