α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
⊢ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y} ∈ 𝓝 a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
⊢ IsOpen {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
refine' isOpen_iff_mem_nhds.mpr fun a ha => _
case h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
b : α
hb : ∀ᶠ (x : α) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : α) in 𝓝[{b}ᶜ] b, p y
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
⊢ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y} ∈ 𝓝 a
filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb
case h.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
hb : ∀ᶠ (x : α) in 𝓝[{a}ᶜ] a, p x
⊢ ∀ᶠ (y : α) in 𝓝[{a}ᶜ] a, p y

case h.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
b : α
hb : ∀ᶠ (x : α) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : α) in 𝓝[{b}ᶜ] b, p y
case h
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
b : α
hb : ∀ᶠ (x : α) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : α) in 𝓝[{b}ᶜ] b, p y
rcases eq_or_ne a b with rfl | h
no goals
case h.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
hb : ∀ᶠ (x : α) in 𝓝[{a}ᶜ] a, p x
⊢ ∀ᶠ (y : α) in 𝓝[{a}ᶜ] a, p y
exact hb
case h.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
b : α
hb : ∀ᶠ (x : α) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : α) in 𝓝[{b}ᶜ] b, p y
case h.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
b : α
hb : ∀ᶠ (x : α) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : α) in 𝓝[{b}ᶜ] b, p y
rw [h.symm.nhdsWithin_compl_singleton] at hb
no goals
case h.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
p : α → Prop
a : α
ha : a ∈ {x | ∀ᶠ (y : α) in 𝓝[{x}ᶜ] x, p y}
b : α
hb : ∀ᶠ (x : α) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : α) in 𝓝[{b}ᶜ] b, p y
exact hb.filter_mono nhdsWithin_le_nhds