ι : Type u_3
κ : Type ?u.130426
X : Type u_4
Y : Type ?u.130432
Z : Type ?u.130435
α : Type u_1
β : Type u_2
γ : Type ?u.130444
𝓕 : Type ?u.130447
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
u : α → β
hu : UniformInducing u
this : ∀ (x : X), EquicontinuousAt F x ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x
⊢ Equicontinuous F ↔ Equicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
ι : Type u_3
κ : Type ?u.130426
X : Type u_4
Y : Type ?u.130432
Z : Type ?u.130435
α : Type u_1
β : Type u_2
γ : Type ?u.130444
𝓕 : Type ?u.130447
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
u : α → β
hu : UniformInducing u
⊢ Equicontinuous F ↔ Equicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
have : ∀ x, EquicontinuousAt F x ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x := by
  intro
  rw [hu.equicontinuousAt_iff]
no goals
ι : Type u_3
κ : Type ?u.130426
X : Type u_4
Y : Type ?u.130432
Z : Type ?u.130435
α : Type u_1
β : Type u_2
γ : Type ?u.130444
𝓕 : Type ?u.130447
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
u : α → β
hu : UniformInducing u
this : ∀ (x : X), EquicontinuousAt F x ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x
⊢ Equicontinuous F ↔ Equicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
exact ⟨fun h x => (this x).mp (h x), fun h x => (this x).mpr (h x)⟩
ι : Type u_3
κ : Type ?u.130426
X : Type u_4
Y : Type ?u.130432
Z : Type ?u.130435
α : Type u_1
β : Type u_2
γ : Type ?u.130444
𝓕 : Type ?u.130447
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
u : α → β
hu : UniformInducing u
x✝ : X
⊢ EquicontinuousAt F x✝ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x✝
ι : Type u_3
κ : Type ?u.130426
X : Type u_4
Y : Type ?u.130432
Z : Type ?u.130435
α : Type u_1
β : Type u_2
γ : Type ?u.130444
𝓕 : Type ?u.130447
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
u : α → β
hu : UniformInducing u
⊢ ∀ (x : X), EquicontinuousAt F x ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x
intro
no goals
ι : Type u_3
κ : Type ?u.130426
X : Type u_4
Y : Type ?u.130432
Z : Type ?u.130435
α : Type u_1
β : Type u_2
γ : Type ?u.130444
𝓕 : Type ?u.130447
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
u : α → β
hu : UniformInducing u
x✝ : X
⊢ EquicontinuousAt F x✝ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x✝
rw [hu.equicontinuousAt_iff]