isEmbedding_postcomp — Mathlib

English

If g: Y → Z is a topological embedding, then postcomposition by g, (g ∘ −): C(X, Y) → C(X, Z), is a topological embedding.

Русский

Если g: Y → Z является топологическим вложением, то посткомпозиция по g, (g ∘ −): C(X, Y) → C(X, Z), сохраняет вложенность.

LaTeX

$$$\\operatorname{IsEmbedding}(g \\circ -)$ provided that $\\operatorname{IsEmbedding}(g)$$$

Lean4

/-- If `g : C(Y, Z)` is a topological embedding,
then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is an embedding too. -/
theorem isEmbedding_postcomp (g : C(Y, Z)) (hg : IsEmbedding g) : IsEmbedding (g.comp : C(X, Y) → C(X, Z)) :=
  ⟨isInducing_postcomp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩

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