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