append — Mathlib

English

Append two embeddings with pairwise disjoint ranges to obtain an embedding of the combined length m+n.

Русский

Объединение двух вложений с непересекающимися образами даёт вложение длины m+n.

LaTeX

$$$\text{append} : (x: \mathrm{Fin}\ m \hookrightarrow \alpha) \to (y: \mathrm{Fin}\ n \hookrightarrow \alpha) \to \mathrm{Fin}\ (m+n) \hookrightarrow \alpha$$$

Lean4

/-- Append a `Fin n ↪ α` at the end of a `Fin m ↪ α` if their ranges are disjoint. -/
def append {m n : ℕ} {x : Fin m ↪ α} {y : Fin n ↪ α} (h : Disjoint (range x) (range y)) : Fin (m + n) ↪ α :=
  ⟨Fin.append x y, Fin.append_injective_iff.mpr ⟨x.inj', y.inj', disjoint_range_iff.mp h⟩⟩

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