α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x✝ y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
refine' ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => _⟩
case intro.intro
α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x✝ y z : α
δ ε ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
case intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
case intro.intro
α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
rcases H ε εpos x hx with ⟨t, ht, Ht⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.79667
ι✝ : Type ?u.79670
inst✝¹ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ : Set α
ι : Type u_1
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩