English
For a distance function d: α → α → ℝ≥0, the infimum over real radii ε > 0 of the principal filters defined by {p ∈ α×α | ↑(d p.1 p.2) < ε} equals the analogous infimum over ε > 0 in ℝ≥0∞. In short, the way we describe closeness using real radii or extended nonnegative radii yields the same infimum description of the uniform structure.
Русский
Для функции расстояния d: α × α → ℝ≥0 разность пределов ε > 0 по реальным радиусам и по ε > 0 в ℝ≥0∞ дают одинаковый результат в виде iInf описания uniformity.
LaTeX
$$$\\inf_{\\varepsilon>0} 𝓟\\{ p:\\ α×α \\mid \\uparrow(d(p_1,p_2))<\\varepsilon\\} = \\inf_{\\varepsilon>0} 𝓟\\{ p:\\ α×α \\mid \\uparrow(d(p_1,p_2))<\\varepsilon\\},$ равносильное выражение через $ℝ_{≥0}^\\infty$.$$
Lean4
theorem uniformity_edist_aux {α} (d : α → α → ℝ≥0) :
⨅ ε > (0 : ℝ), 𝓟 {p : α × α | ↑(d p.1 p.2) < ε} = ⨅ ε > (0 : ℝ≥0∞), 𝓟 {p : α × α | ↑(d p.1 p.2) < ε} :=
by
simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]
refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
· rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩
refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)
exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε
· lift ε to ℝ≥0 using le_of_lt hε
refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)
exact fun _ => ENNReal.coe_lt_coe.1
