[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ →
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
intro H U hU
[GOAL]
case mpr
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ (∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U) →
    EquicontinuousAt F x₀
[PROOFSTEP]
intro H U hU
[GOAL]
case mp
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
H : EquicontinuousAt F x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
[GOAL]
case mp.intro.intro.intro
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
H : EquicontinuousAt F x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
refine' ⟨_, H V hV, fun x hx y hy i => hVU (prod_mk_mem_compRel _ (hy i))⟩
[GOAL]
case mp.intro.intro.intro
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
H : EquicontinuousAt F x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
x : X
hx : x ∈ {x | (fun x => ∀ (i : ι), (F i x₀, F i x) ∈ V) x}
y : X
hy : y ∈ {x | (fun x => ∀ (i : ι), (F i x₀, F i x) ∈ V) x}
i : ι
⊢ (F i x, F i x₀) ∈ V
[PROOFSTEP]
exact hVsymm.mk_mem_comm.mp (hx i)
[GOAL]
case mpr
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
[PROOFSTEP]
rcases H U hU with ⟨V, hV, hVU⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set X
hV : V ∈ 𝓝 x₀
hVU : ∀ (x : X), x ∈ V → ∀ (y : X), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
[PROOFSTEP]
filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhds hV) x hx i
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
⊢ ContinuousAt (F i) x₀
[PROOFSTEP]
intro U hU
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
hU : U ∈ 𝓝 (F i x₀)
⊢ U ∈ map (F i) (𝓝 x₀)
[PROOFSTEP]
rw [UniformSpace.mem_nhds_iff] at hU
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
hU : ∃ V, V ∈ 𝓤 α ∧ ball (F i x₀) V ⊆ U
⊢ U ∈ map (F i) (𝓝 x₀)
[PROOFSTEP]
rcases hU with ⟨V, hV₁, hV₂⟩
[GOAL]
case intro.intro
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
V : Set (α × α)
hV₁ : V ∈ 𝓤 α
hV₂ : ball (F i x₀) V ⊆ U
⊢ U ∈ map (F i) (𝓝 x₀)
[PROOFSTEP]
exact mem_map.mpr (mem_of_superset (h V hV₁) fun x hx => hV₂ (hx i))
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
⊢ EquicontinuousAt Subtype.val x₀
[PROOFSTEP]
rw [← comp_rangeSplitting F]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
⊢ EquicontinuousAt (F ∘ rangeSplitting F) x₀
[PROOFSTEP]
exact h.comp _
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous Subtype.val
[PROOFSTEP]
rw [← comp_rangeSplitting F]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)
[PROOFSTEP]
exact h.comp _
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) x₀
[PROOFSTEP]
rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ (i : Set (α × α)),
      i ∈ 𝓤 α →
        ∀ᶠ (x : X) in 𝓝 x₀,
          (↑UniformFun.ofFun ∘ Function.swap F) x ∈
            {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α i}
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
⊢ Equicontinuous F ↔ Continuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
⊢ UniformEquicontinuous F ↔ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    ∀ (i : Set (α × α)),
      i ∈ 𝓤 α →
        ∀ᶠ (x : β × β) in 𝓤 β,
          ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
            UniformFun.gen ι α i
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → X → α'
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀
[PROOFSTEP]
simp [@equicontinuousAt_iff_continuousAt _ _ _ _ _, UniformFun.topologicalSpace]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → X → α'
x₀ : X
⊢ ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) x₀ ↔
    ∀ (k : κ), ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) x₀
[PROOFSTEP]
unfold ContinuousAt
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → X → α'
x₀ : X
⊢ Tendsto (↑UniformFun.ofFun ∘ Function.swap F) (𝓝 x₀) (𝓝 ((↑UniformFun.ofFun ∘ Function.swap F) x₀)) ↔
    ∀ (k : κ), Tendsto (↑UniformFun.ofFun ∘ Function.swap F) (𝓝 x₀) (𝓝 ((↑UniformFun.ofFun ∘ Function.swap F) x₀))
[PROOFSTEP]
rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F
[PROOFSTEP]
simp_rw [@equicontinuous_iff_continuous _ _ _ _ _, UniformFun.topologicalSpace]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Continuous (↑UniformFun.ofFun ∘ Function.swap F) ↔ ∀ (k : κ), Continuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F
[PROOFSTEP]
simp_rw [@uniformEquicontinuous_iff_uniformContinuous _ _ _ _]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α' : Type u_10
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F) ↔
    ∀ (k : κ), UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
X' : Type u_10
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousAt F x₀
⊢ EquicontinuousAt F x₀
[PROOFSTEP]
simp [@equicontinuousAt_iff_continuousAt _ _ _ _] at hk ⊢
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
X' : Type u_10
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) x₀
⊢ ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) x₀
[PROOFSTEP]
unfold ContinuousAt at hk ⊢
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
X' : Type u_10
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : Tendsto (↑UniformFun.ofFun ∘ Function.swap F) (𝓝 x₀) (𝓝 ((↑UniformFun.ofFun ∘ Function.swap F) x₀))
⊢ Tendsto (↑UniformFun.ofFun ∘ Function.swap F) (𝓝 x₀) (𝓝 ((↑UniformFun.ofFun ∘ Function.swap F) x₀))
[PROOFSTEP]
rw [nhds_iInf]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
X' : Type u_10
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : Tendsto (↑UniformFun.ofFun ∘ Function.swap F) (𝓝 x₀) (𝓝 ((↑UniformFun.ofFun ∘ Function.swap F) x₀))
⊢ Tendsto (↑UniformFun.ofFun ∘ Function.swap F) (⨅ (i : κ), 𝓝 x₀) (𝓝 ((↑UniformFun.ofFun ∘ Function.swap F) x₀))
[PROOFSTEP]
exact tendsto_iInf' k hk
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
X' : Type u_10
t : κ → TopologicalSpace X'
F : ι → X' → α
k : κ
hk : Equicontinuous F
⊢ Equicontinuous F
[PROOFSTEP]
simp_rw [@equicontinuous_iff_continuous _ _ _ _] at hk ⊢
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
X' : Type u_10
t : κ → TopologicalSpace X'
F : ι → X' → α
k : κ
hk : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ Continuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
exact continuous_iInf_dom hk
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
β' : Type u_10
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformEquicontinuous F
⊢ UniformEquicontinuous F
[PROOFSTEP]
simp_rw [@uniformEquicontinuous_iff_uniformContinuous _ _ _ _ _] at hk ⊢
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
β' : Type u_10
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
[PROOFSTEP]
exact uniformContinuous_iInf_dom hk
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
[PROOFSTEP]
rw [equicontinuousAt_iff_continuousAt, ContinuousAt, hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : X),
              x ∈ s ia →
                (↑UniformFun.ofFun ∘ Function.swap F) x ∈
                  {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
[PROOFSTEP]
simp only [Function.comp_apply, mem_setOf_eq, exists_prop]
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : X),
              x ∈ s ia →
                (↑UniformFun.ofFun (Function.swap F x₀), ↑UniformFun.ofFun (Function.swap F x)) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : HasBasis (𝓤 α) p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
[PROOFSTEP]
rw [equicontinuousAt_iff_continuousAt, ContinuousAt, (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : HasBasis (𝓤 α) p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝 x₀,
          (↑UniformFun.ofFun ∘ Function.swap F) x ∈
            {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_10
κ₂ : Type u_11
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
[PROOFSTEP]
rw [equicontinuousAt_iff_continuousAt, ContinuousAt, hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_10
κ₂ : Type u_11
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : X),
              x ∈ s₁ ia →
                (↑UniformFun.ofFun ∘ Function.swap F) x ∈
                  {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
[PROOFSTEP]
simp only [Function.comp_apply, mem_setOf_eq, exists_prop]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_10
κ₂ : Type u_11
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : X),
              x ∈ s₁ ia →
                (↑UniformFun.ofFun (Function.swap F x₀), ↑UniformFun.ofFun (Function.swap F x)) ∈
                  UniformFun.gen ι α (s₂ ib)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ UniformEquicontinuous F ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous, hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : β × β),
              x ∈ s ia →
                ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
simp only [Prod.forall, Function.comp_apply, mem_setOf_eq, exists_prop]
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (a b : β),
              (a, b) ∈ s ia →
                (↑UniformFun.ofFun (Function.swap F a), ↑UniformFun.ofFun (Function.swap F b)) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : HasBasis (𝓤 α) p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ s k
[PROOFSTEP]
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
[GOAL]
ι : Type u_1
κ✝ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_10
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : HasBasis (𝓤 α) p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β,
          ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
            (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ s k
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_10
κ₂ : Type u_11
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : HasBasis (𝓤 β) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
[PROOFSTEP]
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_10
κ₂ : Type u_11
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : HasBasis (𝓤 β) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : β × β),
              x ∈ s₁ ia →
                ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
                  (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
[PROOFSTEP]
simp only [Prod.forall, Function.comp_apply, mem_setOf_eq, exists_prop]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_10
κ₂ : Type u_11
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : HasBasis (𝓤 β) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (a b : β),
              (a, b) ∈ s₁ ia →
                (↑UniformFun.ofFun (Function.swap F a), ↑UniformFun.ofFun (Function.swap F b)) ∈
                  UniformFun.gen ι α (s₂ ib)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x₀
[PROOFSTEP]
have := (UniformFun.postcomp_uniformInducing (α := ι) hu).inducing
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
this : Inducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x₀
[PROOFSTEP]
rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
this : Inducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ ContinuousAt ((↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun) ∘ ↑UniformFun.ofFun ∘ Function.swap F) x₀ ↔
    ContinuousAt (↑UniformFun.ofFun ∘ Function.swap ((fun x x_1 => x ∘ x_1) u ∘ F)) x₀
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
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)
[PROOFSTEP]
have : ∀ x, EquicontinuousAt F x ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x :=
  by
  intro
  rw [hu.equicontinuousAt_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
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
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
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✝
[PROOFSTEP]
rw [hu.equicontinuousAt_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
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)
[PROOFSTEP]
exact
  ⟨fun h x => (this x).mp (h x), fun h x => (this x).mpr (h x)⟩
    -- Porting note: proof was:
      -- congrm (∀ x, _ : Prop)
      -- rw [hu.equicontinuousAt_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
[PROOFSTEP]
have := UniformFun.postcomp_uniformInducing (α := ι) hu
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
this : UniformInducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
[PROOFSTEP]
rw [uniformEquicontinuous_iff_uniformContinuous, uniformEquicontinuous_iff_uniformContinuous,
  this.uniformContinuous_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
this : UniformInducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ UniformContinuous ((↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun) ∘ ↑UniformFun.ofFun ∘ Function.swap F) ↔
    UniformContinuous (↑UniformFun.ofFun ∘ Function.swap ((fun x x_1 => x ∘ x_1) u ∘ F))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
⊢ EquicontinuousAt (u ∘ Subtype.val) x₀
[PROOFSTEP]
intro U hU
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
[PROOFSTEP]
rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
[PROOFSTEP]
filter_upwards [hA V hV] with x hx
[GOAL]
case h
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
⊢ ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
[PROOFSTEP]
rw [SetCoe.forall] at *
[GOAL]
case h
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx :
  ∀ (x_1 : Y) (h : x_1 ∈ A),
    ((u ∘ Subtype.val) { val := x_1, property := h } x₀, (u ∘ Subtype.val) { val := x_1, property := h } x) ∈ V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A),
    ((u ∘ Subtype.val) { val := x_1, property := h } x₀, (u ∘ Subtype.val) { val := x_1, property := h } x) ∈ U
[PROOFSTEP]
change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx
[GOAL]
case h
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A),
    ((u ∘ Subtype.val) { val := x_1, property := h } x₀, (u ∘ Subtype.val) { val := x_1, property := h } x) ∈ U
[PROOFSTEP]
refine' (closure_minimal hx <| hVclosed.preimage <| _).trans (preimage_mono hVU)
[GOAL]
case h
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V
⊢ Continuous fun f => (u f x₀, u f x)
[PROOFSTEP]
exact Continuous.prod_mk ((continuous_apply x₀).comp hu) ((continuous_apply x).comp hu)
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
⊢ UniformEquicontinuous (u ∘ Subtype.val)
[PROOFSTEP]
intro U hU
[GOAL]
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i xy.fst, (u ∘ Subtype.val) i xy.snd) ∈ U
[PROOFSTEP]
rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
⊢ ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i xy.fst, (u ∘ Subtype.val) i xy.snd) ∈ U
[PROOFSTEP]
filter_upwards [hA V hV]
[GOAL]
case h
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
⊢ ∀ (a : β × β),
    (∀ (i : ↑A), ((u ∘ Subtype.val) i a.fst, (u ∘ Subtype.val) i a.snd) ∈ V) →
      ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i a.fst, (u ∘ Subtype.val) i a.snd) ∈ U
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case h.mk
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxy : ∀ (i : ↑A), ((u ∘ Subtype.val) i (x, y).fst, (u ∘ Subtype.val) i (x, y).snd) ∈ V
⊢ ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i (x, y).fst, (u ∘ Subtype.val) i (x, y).snd) ∈ U
[PROOFSTEP]
rw [SetCoe.forall] at *
[GOAL]
case h.mk
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxy :
  ∀ (x_1 : Y) (h : x_1 ∈ A),
    ((u ∘ Subtype.val) { val := x_1, property := h } (x, y).fst,
        (u ∘ Subtype.val) { val := x_1, property := h } (x, y).snd) ∈
      V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A),
    ((u ∘ Subtype.val) { val := x_1, property := h } (x, y).fst,
        (u ∘ Subtype.val) { val := x_1, property := h } (x, y).snd) ∈
      U
[PROOFSTEP]
change A ⊆ (fun f => (u f x, u f y)) ⁻¹' V at hxy
[GOAL]
case h.mk
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxy : A ⊆ (fun f => (u f x, u f y)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A),
    ((u ∘ Subtype.val) { val := x_1, property := h } (x, y).fst,
        (u ∘ Subtype.val) { val := x_1, property := h } (x, y).snd) ∈
      U
[PROOFSTEP]
refine' (closure_minimal hxy <| hVclosed.preimage <| _).trans (preimage_mono hVU)
[GOAL]
case h.mk
ι : Type u_1
κ : Type u_2
X : Type u_3
Y : Type u_4
Z : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
𝓕 : Type u_9
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (u ∘ Subtype.val)
hu : Continuous u
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x y : β
hxy : A ⊆ (fun f => (u f x, u f y)) ⁻¹' V
⊢ Continuous fun f => (u f x, u f y)
[PROOFSTEP]
exact Continuous.prod_mk ((continuous_apply x).comp hu) ((continuous_apply y).comp hu)


[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
x : X
⊢ HolderOnWith C r f {x}
[PROOFSTEP]
rintro a (rfl : a = x) b (rfl : b = a)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
b : X
⊢ edist (f b) (f b) ≤ ↑C * edist b b ^ ↑r
[PROOFSTEP]
rw [edist_self]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
b : X
⊢ 0 ≤ ↑C * edist b b ^ ↑r
[PROOFSTEP]
exact zero_le _
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
⊢ HolderOnWith C r f univ ↔ HolderWith C r f
[PROOFSTEP]
simp only [HolderOnWith, HolderWith, mem_univ, true_imp_iff]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C : ℝ≥0
f : X → Y
s : Set X
⊢ HolderOnWith C 1 f s ↔ LipschitzOnWith C f s
[PROOFSTEP]
simp only [HolderOnWith, LipschitzOnWith, NNReal.coe_one, ENNReal.rpow_one]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f✝ : X → Y
s t✝ : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
⊢ HolderOnWith (Cg * NNReal.rpow Cf ↑rg) (rg * rf) (g ∘ f) s
[PROOFSTEP]
intro x hx y hy
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f✝ : X → Y
s t✝ : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑(Cg * NNReal.rpow Cf ↑rg) * edist x y ^ ↑(rg * rf)
[PROOFSTEP]
rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc, NNReal.rpow_eq_pow, ←
  ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f✝ : X → Y
s t✝ : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑Cg * (↑Cf * edist x y ^ ↑rf) ^ ↑rg
[PROOFSTEP]
exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
⊢ UniformContinuousOn f s
[PROOFSTEP]
refine' EMetric.uniformContinuousOn_iff.2 fun ε εpos => _
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
[PROOFSTEP]
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
  ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top h0
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
[PROOFSTEP]
rcases ENNReal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ (fun d => ↑C * d ^ ↑r) ⁻¹' {x | (fun x => x < ε) x}
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
[PROOFSTEP]
exact ⟨δ, δ0, fun hx y hy h => (hf.edist_le hx hy).trans_lt (H h)⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ ↑(nndist (f x) (f y)) ≤ ↑C * ↑d ^ ↑r
[PROOFSTEP]
norm_cast
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r
[PROOFSTEP]
rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul, ← ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
[PROOFSTEP]
apply hf.edist_le_of_le
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist x y ≤ ↑d
[PROOFSTEP]
rwa [edist_nndist, ENNReal.coe_le_coe]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ
hd : dist x y ≤ d
⊢ dist (f x) (f y) ≤ ↑C * d ^ ↑r
[PROOFSTEP]
lift d to ℝ≥0 using dist_nonneg.trans hd
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : dist x y ≤ ↑d
⊢ dist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
[PROOFSTEP]
rw [dist_nndist] at hd ⊢
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : ↑(nndist x y) ≤ ↑d
⊢ ↑(nndist (f x) (f y)) ≤ ↑C * ↑d ^ ↑r
[PROOFSTEP]
norm_cast at hd ⊢
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r
[PROOFSTEP]
exact hf.nndist_le_of_le hd