isClosedEmbedding_coe — Mathlib

English

The coe map from MonoidHom to the underlying function is a closed embedding, under discreteness and separation assumptions on the domain and target.

Русский

Отображение коe из MonoidHom в базовую функцию является замкнутым вложением при дискретности и требуемой разделимости пространства.

LaTeX

$$$\mathrm{IsClosedEmbedding}( (\!\!\!\!\! ) : (A \to\* B) \to A \to B )$$$

Lean4

@[to_additive]
theorem isClosedEmbedding_coe : IsClosedEmbedding ((⇑) : (A →ₜ* B) → A → B) :=
  ContinuousMap.isHomeomorph_coe.isClosedEmbedding.comp <| isClosedEmbedding_toContinuousMap ..

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