isUniformEmbedding_toProdMulOpposite

English

The map toProdMulOpposite is a uniform embedding, i.e., it is an injective map that preserves uniform structures.

Русский

Отображение toProdMulOpposite является равномерным вложением: инъекция, сохраняющая равномерную структуру пространства.

LaTeX

$$$\text{IsUniformEmbedding}(\mathrm{toProdMulOpposite})$$$

Lean4

theorem isUniformEmbedding_toProdMulOpposite : IsUniformEmbedding (toProdMulOpposite (𝕜 := 𝕜) (A := A)) :=
  isUniformEmbedding_comap toProdMulOpposite_injective

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