isClosedEmbedding — Mathlib

English

The map I is a closed embedding: it is an embedding whose image is a closed subset of the target space.

Русский

Отображение I является замкнутым вложением: оно инъективно (образ является замкнутым подмножеством целевого пространства).

LaTeX

$$IsClosedEmbedding(I.toFun')$$

Lean4

theorem isClosedEmbedding : IsClosedEmbedding I :=
  I.leftInverse.isClosedEmbedding I.continuous_symm I.continuous

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