case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s t : Set α
hu : t ⊆ insert x s
⊢ insert x s ∈ 𝓝[t] x

case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
⊢ insert x s ∈ 𝓝[t] x
rcases eq_or_ne x y with (rfl | h)
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[insert y s] x
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x
refine' nhdsWithin_mono x hu _
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[insert y s] x
rw [nhdsWithin_insert_of_ne h]
no goals
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x y : α
s t : Set α
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x
exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)
no goals
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
x : α
s t : Set α
hu : t ⊆ insert x s
⊢ insert x s ∈ 𝓝[t] x
exact mem_of_superset self_mem_nhdsWithin hu