update_apply_of_injective — Mathlib

English

If f is injective, then for all i, a, j, the value of update g (f i) a (f j) equals the value of update (k ↦ g (f k)) i a at j.

Русский

Если f инъективна, то для любых i, a, j имеет место равенство: update g (f i) a (f j) = update (λk, g(f k)) i a j.

LaTeX

$$$\\forall i,a,j,\\ update g (f i) a (f j) = \\ big(\\mathrm{update}(k \\mapsto g(f k))\\ i\\ a\\big)(j)$$$

Lean4

theorem update_apply_of_injective (g : ∀ a, β a) {f : α' → α} (hf : Function.Injective f) (i : α') (a : β (f i))
    (j : α') : update g (f i) a (f j) = update (fun i ↦ g (f i)) i a j :=
  congr_fun (update_comp_eq_of_injective' g hf i a) j

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