α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔
    ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
rw [equicontinuousAt_iff_pair]
case mp
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε

case mpr
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
constructor <;> intro H
case mp
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
ε : ℝ
hε : ε > 0
⊢ ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
case mp
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
intro ε hε
no goals
case mp
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
ε : ℝ
hε : ε > 0
⊢ ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
exact H _ (dist_mem_uniformity hε)
case mpr
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
case mpr
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
intro U hU
case mpr.intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ {a b : α}, dist a b < ε → (a, b) ∈ U
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
case mpr
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
case mpr.intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ {a b : α}, dist a b < ε → (a, b) ∈ U
V : Set β
h : ∀ (x : β), x ∈ V → ∀ (x' : β), x' ∈ V → ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
case mpr.intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ {a b : α}, dist a b < ε → (a, b) ∈ U
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
refine' Exists.imp (fun V => And.imp_right fun h => _) (H _ hε)
no goals
case mpr.intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.1103
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ {a b : α}, dist a b < ε → (a, b) ∈ U
V : Set β
h : ∀ (x : β), x ∈ V → ∀ (x' : β), x' ∈ V → ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)