isEmbedding_toContinuousMap — Mathlib

English

The map toContinuousMap is an embedding; i.e., it is an inducing map and injective.

Русский

Отображение toContinuousMap является вложением: оно индуктивно и инъективно.

LaTeX

$$$\mathrm{IsEmbedding}(\mathrm{toContinuousMap})$.$$

Lean4

@[to_additive]
theorem isEmbedding_toContinuousMap : IsEmbedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
  ⟨isInducing_toContinuousMap A B, toContinuousMap_injective⟩

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