α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
⊢ IsOpen {x}
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
⊢ IsOpen {x}
have A : {x} ⊆ s := by simp only [singleton_subset_iff, mem_of_mem_nhds hs]
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
⊢ IsOpen {x}
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
⊢ IsOpen {x}
have B : IsClosed (s \ {x}) := (hsf.subset (diff_subset _ _)).isClosed
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen {x}
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
⊢ IsOpen {x}
have C : (s \ {x})ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
⊢ IsOpen {x}
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen {x}
have D : {x} ∈ 𝓝 x := by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C
no goals
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
⊢ IsOpen {x}
rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D
no goals
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
⊢ {x} ⊆ s
simp only [singleton_subset_iff, mem_of_mem_nhds hs]
no goals
α✝ : Type u
β : Type v
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s : Set α
hs : s ∈ 𝓝 x
hsf : Set.Finite s
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ {x} ∈ 𝓝 x
simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C