update_comp_eq_of_forall_ne — Mathlib

English

If every value f x is not equal to i, then update g i a composed with f equals g composed with f.

Русский

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

LaTeX

$$$\\big(\\mathrm{update}\\ g\\ i\\ a\\big) \\circ f = g \\circ f\\quad \\text{if } \\forall x, f x \\neq i$$$

Lean4

/-- Non-dependent version of `Function.update_comp_eq_of_forall_ne'` -/
theorem update_comp_eq_of_forall_ne {α β : Sort*} (g : α' → β) {f : α → α'} {i : α'} (a : β) (h : ∀ x, f x ≠ i) :
    update g i a ∘ f = g ∘ f :=
  update_comp_eq_of_forall_ne' g a h

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