isEmbedding_embedProduct — Mathlib

English

Let M be a topological monoid. The natural map embedProduct M : Mˣ → M × M sending a unit u to (val(u), val(u)^{-1}) is a topological embedding.

Русский

Пусть M — топологическая полугруппа. Натуральное отображение embedProduct M : Mˣ → M × M, отображающее единицу u в (val(u), val(u)^{-1}), является топологическим вложением.

LaTeX

$$$\\mathrm{IsEmbedding}(\\mathrm{embedProduct}\, M)$$$

Lean4

@[to_additive]
theorem isEmbedding_embedProduct : IsEmbedding (embedProduct M) :=
  ⟨isInducing_embedProduct, embedProduct_injective M⟩

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