comp — Mathlib

English

If g and f are embeddings, then their composition g ∘ f is an embedding.

Русский

Если g и f являются вложениями, то их композиция g ∘ f является вложением.

LaTeX

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

Lean4

protected theorem comp (hg : IsEmbedding g) (hf : IsEmbedding f) : IsEmbedding (g ∘ f) :=
  { hg.isInducing.comp hf.isInducing with injective := fun _ _ h => hf.injective <| hg.injective h }

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