α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ s ⊆ interior s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
rw [← subset_interior_iff_isOpen]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ s ⊆ interior s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
simp only [subset_def, mem_interior]