uniformEmbedding_ofMatrix — Mathlib

English

The map ofMatrix from Matrix m n A to CStarMatrix m n A is a uniform embedding; it is injective and respects the uniformity.

Русский

Отображение ofMatrix из Matrix m n A в CStarMatrix m n A является равномерным вложением; оно инъективно и сохраняет равномерность.

LaTeX

$$$$\\text{IsUniformEmbedding}(\\mathrm{ofMatrix}).$$$$

Lean4

theorem uniformEmbedding_ofMatrix : IsUniformEmbedding (ofMatrix : Matrix m n A → CStarMatrix m n A)
    where
  comap_uniformity := Filter.comap_id'
  injective := fun ⦃_ _⦄ a ↦ a

Похожие утверждения