α : Type u
β : Type v
γ : Type ?u.159306
δ : Type ?u.159309
ε : Type ?u.159312
ζ : Type ?u.159315
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
a : α
ha : p a
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ (fun x => p x) ∈ 𝓝 ↑{ val := a, property := ha }
α : Type u
β : Type v
γ : Type ?u.159306
δ : Type ?u.159309
ε : Type ?u.159312
ζ : Type ?u.159315
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
a : α
ha : p a
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ range Subtype.val ∈ 𝓝 ↑{ val := a, property := ha }
rw [Subtype.range_val]
no goals
α : Type u
β : Type v
γ : Type ?u.159306
δ : Type ?u.159309
ε : Type ?u.159312
ζ : Type ?u.159315
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
a : α
ha : p a
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ (fun x => p x) ∈ 𝓝 ↑{ val := a, property := ha }
exact h