case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)
have : UniformContinuousOn (↿f) (K ×ˢ univ) :=
  IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ)
    (h.mono <| prod_mono hKU Subset.rfl)
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : CompactSpace β
inst✝ : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (U ×ˢ univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
this : UniformContinuousOn (↿f) (K ×ˢ univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
exact this.tendstoUniformly hxK