α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
⊢ (∀ (a : Set α) (b : Set (β × β)), IsCompact a → b ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ compactConvNhd a b f) ↔
    ∀ (K : Set α), IsCompact K → ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ K → (↑f x, ↑(F n) x) ∈ u
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
⊢ Tendsto F p (𝓝 f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
simp only [(hasBasis_nhds_compactConvergence f).tendsto_right_iff, TendstoUniformlyOn, and_imp,
  Prod.forall]
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
K : Set α
⊢ (∀ (b : Set (β × β)), IsCompact K → b ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ compactConvNhd K b f) ↔
    IsCompact K → ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ K → (↑f x, ↑(F n) x) ∈ u
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
⊢ (∀ (a : Set α) (b : Set (β × β)), IsCompact a → b ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ compactConvNhd a b f) ↔
    ∀ (K : Set α), IsCompact K → ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ K → (↑f x, ↑(F n) x) ∈ u
refine' forall_congr' fun K => _
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
K : Set α
⊢ (IsCompact K → ∀ (x : Set (β × β)), x ∈ 𝓤 β → ∀ᶠ (x_1 : ι) in p, F x_1 ∈ compactConvNhd K x f) ↔
    IsCompact K → ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ K → (↑f x, ↑(F n) x) ∈ u
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
K : Set α
⊢ (∀ (b : Set (β × β)), IsCompact K → b ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ compactConvNhd K b f) ↔
    IsCompact K → ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ K → (↑f x, ↑(F n) x) ∈ u
rw [forall_swap]
no goals
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
K : Set α
⊢ (IsCompact K → ∀ (x : Set (β × β)), x ∈ 𝓤 β → ∀ᶠ (x_1 : ι) in p, F x_1 ∈ compactConvNhd K x f) ↔
    IsCompact K → ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ K → (↑f x, ↑(F n) x) ∈ u
exact forall₃_congr fun _hK V _hV => Iff.rfl