Embedding (埋め込み) (Definition IV.3.12)

• Embedding (埋め込み) (Definition IV.3.12) #Card
  • An injective map is called an embedding if its domain and its range are homeomorphic: $f : \eta \hookrightarrow \xi$ if $f \in C(\eta, \xi)$ and $i \in H(\eta, f^-\xi)$.

Back

An injective map is called an embedding if its domain and its range are homeomorphic. Explicitly, $f$ is an embedding of $\eta$ in $\xi$, written $$f : \eta \hookrightarrow \xi,$$ if $f \in C(\eta, \xi)$ and the identity $i \in H(\eta, f^-\xi)$（つまり $\eta$ が $f$ による始収束と一致する単射連続写像）.

• 一部の著者（Engelking 等）はこれを homeomorphic embedding と呼ぶ。
• 埋め込みの典型: 単射族に対する diagonal product は積への埋め込み（cards/topology/prop-iv-7-7）。

Lean

位相の場合 Topology.IsEmbedding f（IsInducing + Injective）