English
The uniformity on Matrix m n 𝕜 is the infimum of the comaplications of the uniformity on 𝕜 along the coordinate projections, i.e., 𝓤(Matrix m n 𝕜) = ⨅ i j, (𝓤 𝕜).comap (a ↦ (a.i j, a'.i j)).
Русский
Унитерность пространства матриц m×n над 𝕜 равна инфимуму по координатам проекций от униформности 𝕜: 𝓤(Matrix m n 𝕜) = ⨅ i j, (𝓤 𝕜).comap ….
LaTeX
$$$\mathcal{U}(\mathrm{Matrix}\ m\ n\ 𝕜) = \bigwedge_{i:\;m}\bigwedge_{j:\;n} (\mathcal{U}(𝕜)).\mathrm{comap}\big(\lambda a,(a,i,j)\mapsto (a_{i j}, a'_{i j})\big)$$$
Lean4
theorem uniformity : 𝓤 (Matrix m n 𝕜) = ⨅ (i : m) (j : n), (𝓤 𝕜).comap fun a => (a.1 i j, a.2 i j) :=
by
erw [Pi.uniformity]
simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap]
rfl
