case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s →
    ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε

case mpr
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
⊢ (∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε) →
    UniformCauchySeqOn F atTop s
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s ↔
    ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
constructor
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s →
    ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
intro h ε hε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
⊢ ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
let u := { a : α × α | dist a.fst a.snd < ε }
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
⊢ ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
⊢ ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp⟩
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ (x_1 : γ), x_1 ∈ s → dist (F x.fst x_1) (F x.snd x_1) < ε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
⊢ ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
rw [← @Filter.eventually_atTop_prod_self' _ _ _ fun m =>
  ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε]
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
⊢ ∀ᶠ (x : β × β) in atTop, ∀ (x_1 : γ), x_1 ∈ s → dist (F x.fst x_1) (F x.snd x_1) < ε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ (x_1 : γ), x_1 ∈ s → dist (F x.fst x_1) (F x.snd x_1) < ε
specialize h u hu
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
⊢ ∀ᶠ (x : β × β) in atTop, ∀ (x_1 : γ), x_1 ∈ s → dist (F x.fst x_1) (F x.snd x_1) < ε
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
⊢ ∀ᶠ (x : β × β) in atTop, ∀ (x_1 : γ), x_1 ∈ s → dist (F x.fst x_1) (F x.snd x_1) < ε
rw [prod_atTop_atTop_eq] at h
no goals
case mp
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
hu : u ∈ 𝓤 α
h : ∀ᶠ (m : β × β) in atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
⊢ ∀ᶠ (x : β × β) in atTop, ∀ (x_1 : γ), x_1 ∈ s → dist (F x.fst x_1) (F x.snd x_1) < ε
exact h.mono fun n h x hx => h x hx
no goals
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.fst a.snd < ε}
⊢ ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
simp
case mpr
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
case mpr
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
⊢ (∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε) →
    UniformCauchySeqOn F atTop s
intro h u hu
case mpr.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
case mpr
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
case mpr.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
rcases h ε hε with ⟨N, hN⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
⊢ ∃ a, ∀ (b : β × β), b ≥ a → ∀ (x : γ), x ∈ s → (F b.fst x, F b.snd x) ∈ u
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ (x : γ), x ∈ s → (F m.fst x, F m.snd x) ∈ u
rw [prod_atTop_atTop_eq, eventually_atTop]
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
⊢ ∀ (b : β × β), b ≥ (N, N) → ∀ (x : γ), x ∈ s → (F b.fst x, F b.snd x) ∈ u
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
⊢ ∃ a, ∀ (b : β × β), b ≥ a → ∀ (x : γ), x ∈ s → (F b.fst x, F b.snd x) ∈ u
use (N, N)
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
b : β × β
hb : b ≥ (N, N)
x : γ
hx : x ∈ s
⊢ (F b.fst x, F b.snd x) ∈ u
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
⊢ ∀ (b : β × β), b ≥ (N, N) → ∀ (x : γ), x ∈ s → (F b.fst x, F b.snd x) ∈ u
intro b hb x hx
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
b : β × β
x : γ
hx : x ∈ s
hbl : (N, N).fst ≤ b.fst
hbr : (N, N).snd ≤ b.snd
⊢ (F b.fst x, F b.snd x) ∈ u
case mpr.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
b : β × β
hb : b ≥ (N, N)
x : γ
hx : x ∈ s
⊢ (F b.fst x, F b.snd x) ∈ u
rcases hb with ⟨hbl, hbr⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.218356
ι : Type ?u.218359
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_1
F : β → γ → α
s : Set γ
h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε
b : β × β
x : γ
hx : x ∈ s
hbl : (N, N).fst ≤ b.fst
hbr : (N, N).snd ≤ b.snd
⊢ (F b.fst x, F b.snd x) ∈ u
exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)