sumMap — Mathlib

English

If e1: α ↪ β and e2: γ ↪ δ are embeddings, then Sum.map e1 e2 is an embedding α ⊕ γ ↪ β ⊕ δ.

Русский

Если e1: α ↪ β и e2: γ ↪ δ — вложения, то Sum.map e1 e2 — вложение α ⊕ γ ↪ β ⊕ δ.

LaTeX

$$$\\mathrm{sumMap}(e_1,e_2): \\alpha \\oplus \\gamma \\hookrightarrow \\beta \\oplus \\delta,\\; (\\mathrm{inl}\\ a) \\mapsto \\mathrm{inl}(e_1 a),\\; (\\mathrm{inr}\\ c) \\mapsto \\mathrm{inr}(e_2 c)$$$

Lean4

/-- If `e₁` and `e₂` are embeddings, then so is `Sum.map e₁ e₂`. -/
def sumMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ⊕ γ ↪ β ⊕ δ :=
  ⟨Sum.map e₁ e₂, e₁.injective.sumMap e₂.injective⟩

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