comp — Mathlib

English

The composition of two closed embeddings is a closed embedding.

Русский

Сложение (композиция) двух замкнутых вложений образует замкнутое вложение.

LaTeX

$$$\mathrm{IsClosedEmbedding}(g) \rightarrow \mathrm{IsClosedEmbedding}(f) \rightarrow \mathrm{IsClosedEmbedding}(g \circ f)$$$

Lean4

theorem comp (hg : IsClosedEmbedding g) (hf : IsClosedEmbedding f) : IsClosedEmbedding (g ∘ f) :=
  ⟨hg.isEmbedding.comp hf.isEmbedding, (hg.isClosedMap.comp hf.isClosedMap).isClosed_range⟩

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