update_comp_eq_of_notMem_range — Mathlib

English

A non-dependent version: update g i a ∘ f = g ∘ f when i ∉ range f.

Русский

Независимая от типа зависимостей версия: обновление g в позиции i и композиция с f равны g ∘ f, если i не принадлежит range f.

LaTeX

$$$ \\forall {α β} {γ} [DecidableEq β] (g : β \\to γ) {f : α \\to β} {i : β} (a : γ) (h : i \\notin \\operatorname{range} f) : (update g i a) \\circ f = g \\circ f. $$$

Lean4

/-- Non-dependent version of `Function.update_comp_eq_of_notMem_range'` -/
theorem update_comp_eq_of_notMem_range {α : Sort*} {β : Type*} {γ : Sort*} [DecidableEq β] (g : β → γ) {f : α → β}
    {i : β} (a : γ) (h : i ∉ Set.range f) : update g i a ∘ f = g ∘ f :=
  update_comp_eq_of_notMem_range' g a h

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