α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ (∀ (i : Set α), Tendsto F p (𝓝 f)) ↔ ∀ (s : Set α), s ∈ 𝔖 → TendstoUniformlyOn F f p s
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ Tendsto F p (𝓝 f) ↔ ∀ (s : Set α), s ∈ 𝔖 → TendstoUniformlyOn F f p s
rw [UniformOnFun.topologicalSpace_eq, nhds_iInf, tendsto_iInf]
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
⊢ Tendsto F p (𝓝 f) ↔ s ∈ 𝔖 → TendstoUniformlyOn F f p s
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ (∀ (i : Set α), Tendsto F p (𝓝 f)) ↔ ∀ (s : Set α), s ∈ 𝔖 → TendstoUniformlyOn F f p s
refine' forall_congr' fun s => _
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
⊢ s ∈ 𝔖 → Tendsto F p (𝓝 f) ↔ s ∈ 𝔖 → TendstoUniformlyOn F f p s
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
⊢ Tendsto F p (𝓝 f) ↔ s ∈ 𝔖 → TendstoUniformlyOn F f p s
rw [nhds_iInf, tendsto_iInf]
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
hs : s ∈ 𝔖
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformlyOn F f p s
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
⊢ s ∈ 𝔖 → Tendsto F p (𝓝 f) ↔ s ∈ 𝔖 → TendstoUniformlyOn F f p s
refine' forall_congr' fun hs => _
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
hs : s ∈ 𝔖
⊢ TendstoUniformly ((restrict s ∘ ↑UniformFun.toFun) ∘ F) ((restrict s ∘ ↑UniformFun.toFun) f) p ↔
    TendstoUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
hs : s ∈ 𝔖
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformlyOn F f p s
rw [nhds_induced (T := _), tendsto_comap_iff, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe,
  UniformFun.tendsto_iff_tendstoUniformly]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.103872
ι : Type u_3
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
hs : s ∈ 𝔖
⊢ TendstoUniformly ((restrict s ∘ ↑UniformFun.toFun) ∘ F) ((restrict s ∘ ↑UniformFun.toFun) f) p ↔
    TendstoUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
rfl