update_comp_eq_of_forall_ne' — Mathlib

English

If f has no values equal to i, then composing with an update on g at i is the same as updating the composed g.

Русский

Если для всех x выполняется f x ≠ i, то композиция с обновлением g i a равна обновлению композиции g через f.

LaTeX

$$$\\ (\\forall x, f x \\neq i) \\Rightarrow (\\lambda j, update\\ g\\ i\\ a\\ (f j)) = (\\lambda j, g( f j))$$$

Lean4

theorem update_comp_eq_of_forall_ne' {α'} (g : ∀ a, β a) {f : α' → α} {i : α} (a : β i) (h : ∀ x, f x ≠ i) :
    (fun j ↦ (update g i a) (f j)) = fun j ↦ g (f j) :=
  funext fun _ ↦ update_of_ne (h _) _ _

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