prodMap — Mathlib

English

If e1: α ↪ β and e2: γ ↪ δ are embeddings, then Prod.map e1 e2 is an embedding α × γ ↪ β × δ, sending (a,c) ↦ (e1 a, e2 c).

Русский

Если e1: α ↪ β и e2: γ ↪ δ — вложения, то Prod.map e1 e2 — вложение α × γ ↪ β × δ, отображающее (a,c) ↦ (e1 a, e2 c).

LaTeX

$$$\\mathrm{prodMap}(e_1,e_2): \\alpha \\times \\gamma \\hookrightarrow \\beta \\times \\delta,\\; (a,c) \\mapsto (e_1(a), e_2(c))$$$

Lean4

/-- If `e₁` and `e₂` are embeddings, then so is `Prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b)`. -/
def prodMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α × γ ↪ β × δ :=
  ⟨Prod.map e₁ e₂, e₁.injective.prodMap e₂.injective⟩

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