α : Type u_1
β : Type u_2
γ : Type ?u.23663
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
α : Type u_1
β : Type u_2
γ : Type ?u.23663
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
rw [compactOpen_eq_sInf_induced]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.23663
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
simp [nhds_iInf, nhds_induced]