insertNth_eq_iff — Mathlib

English

An equality g = p.insertNth a f holds if and only if the inserted value at p is a and the remainder equals the removed tail: f = removeNth p g.

Русский

Равенство g = p.insertNth a f получено тогда, когда вставленное значение в p равно a, а остаток равен удалённому хвосту: f = removeNth p g.

LaTeX

$$g = p.insertNth a f \iff a = g p \land f = removeNth p g$$

Lean4

theorem insertNth_eq_iff {p : Fin (n + 1)} {a : α p} {f : ∀ i, α (p.succAbove i)} {g : ∀ j, α j} :
    insertNth p a f = g ↔ a = g p ∧ f = removeNth p g := by simp [funext_iff, forall_iff_succAbove p, removeNth]

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