α : Type u_2
β : Type u_3
γ : Type ?u.29261
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
α : Type u_2
β : Type u_3
γ : Type ?u.29261
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
rw [compactOpen_eq_sInf_induced]
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.29261
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_1
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp]