English
The distance on Open subset CompleteCopy s is given by dist x y = dist x.1 y.1 + |1/infDist x.1 sᶜ − 1/infDist y.1 sᶜ|.
Русский
Расстояние на открытом подмножестве CompleteCopy s задаётся как dist x y = dist x.1 y.1 + |1/infDist x.1 sᶜ − 1/infDist y.1 sᶜ|.
LaTeX
$$$$\\\\dist(x,y)=\\\\dist(x.\\\\1, y.\\\\1) + \\\\left|\\\\frac{1}{\\\\infDist(x.\\\\1, s^c)} - \\\\frac{1}{\\\\infDist(y.\\\\1, s^c)}\\\\right|.$$$$
Lean4
protected theorem _root_.CompletePseudometrizable.iInf {ι : Type*} [Countable ι] {t : ι → TopologicalSpace α}
(ht₀ : ∃ t₀, @T2Space α t₀ ∧ ∀ i, t i ≤ t₀)
(ht : ∀ i, ∃ u : UniformSpace α, CompleteSpace α ∧ 𝓤[u].IsCountablyGenerated ∧ u.toTopologicalSpace = t i) :
∃ u : UniformSpace α, CompleteSpace α ∧ 𝓤[u].IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i :=
by
choose u hcomp hcount hut using ht
obtain rfl : t = fun i ↦ (u i).toTopologicalSpace := (funext hut).symm
refine ⟨⨅ i, u i, .iInf hcomp ht₀, ?_, UniformSpace.toTopologicalSpace_iInf⟩
rw [iInf_uniformity]
infer_instance
