eq_insertNth_iff — Mathlib

English

An equality g = p.insertNth a f is equivalent to g p = a ∧ removeNth p g = f.

Русский

Равенство g = p.insertNth a f эквивалентно g(p) = a и removeNth p g = f.

LaTeX

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

Lean4

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

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