English
If each E_n has the discrete uniformity, then Π_n E_n carries a metric with the same distance rule.
Русский
Если каждая E_n имеет дискретную униформность, то произведение Π_n E_n несёт метричную структуру с той же формулой расстояния.
LaTeX
$$$$ \text{dist}(x,y) = \begin{cases}0, & x=y \\ (1/2)^{\operatorname{firstDiff}(x,y)}, & x\neq y\end{cases} $$$$
Lean4
/-- Metric space structure on `Π (n : ℕ), E n` when the spaces `E n` have the discrete uniformity,
where the distance is given by `dist x y = (1/2)^n`, where `n` is the smallest index where `x` and
`y` differ. Not registered as a global instance by default. -/
protected def metricSpaceOfDiscreteUniformity {E : ℕ → Type*} [∀ n, UniformSpace (E n)]
(h : ∀ n, uniformity (E n) = 𝓟 idRel) : MetricSpace (∀ n, E n) :=
haveI : ∀ n, DiscreteTopology (E n) := fun n => discreteTopology_of_discrete_uniformity (h n)
{ dist_triangle := PiNat.dist_triangle
dist_comm := PiNat.dist_comm
dist_self := PiNat.dist_self
eq_of_dist_eq_zero := PiNat.eq_of_dist_eq_zero _ _
toUniformSpace := Pi.uniformSpace _
uniformity_dist := by
simp only [Pi.uniformity, h, idRel, comap_principal, preimage_setOf_eq]
apply le_antisymm
· simp only [le_iInf_iff, le_principal_iff]
intro ε εpos
obtain ⟨n, hn⟩ : ∃ n, (1 / 2 : ℝ) ^ n < ε := exists_pow_lt_of_lt_one εpos (by norm_num)
apply
@mem_iInf_of_iInter _ _ _ _ _ (Finset.range n).finite_toSet fun i =>
{p : (∀ n : ℕ, E n) × ∀ n : ℕ, E n | p.fst i = p.snd i}
· simp only [mem_principal, setOf_subset_setOf, imp_self, imp_true_iff]
· rintro ⟨x, y⟩ hxy
simp only [Finset.mem_coe, Finset.mem_range, iInter_coe_set, mem_iInter, mem_setOf_eq] at hxy
apply lt_of_le_of_lt _ hn
rw [← mem_cylinder_iff_dist_le, mem_cylinder_iff]
exact hxy
· simp only [le_iInf_iff, le_principal_iff]
intro n
refine mem_iInf_of_mem ((1 / 2) ^ n : ℝ) ?_
refine mem_iInf_of_mem (by positivity) ?_
simp only [mem_principal, setOf_subset_setOf, Prod.forall]
intro x y hxy
exact apply_eq_of_dist_lt hxy le_rfl }
