update_comp_eq_of_notMem_range' — Mathlib

English

If g is defined on β and i is not in the range of f, then updating g at i and composing with f yields the same result as g ∘ f.

Русский

Если g определена на β и i не принадлежит диапазону f, то обновление g в позиции i затем композиция с f равно g ∘ f.

LaTeX

$$$ {α : Sort*} {β : Type*} {γ : β \\to Sort*} [DecidableEq β] (g : ∀ b, γ b) \\{f : α \\to β\\} {i : β} (a : γ i) (h : i \\notin \\operatorname{range} f) : (fun j => update g i a (f j)) = fun j => g (f j). $$$

Lean4

theorem update_comp_eq_of_notMem_range' {α : Sort*} {β : Type*} {γ : β → Sort*} [DecidableEq β] (g : ∀ b, γ b)
    {f : α → β} {i : β} (a : γ i) (h : i ∉ Set.range f) : (fun j => update g i a (f j)) = fun j => g (f j) :=
  (update_comp_eq_of_forall_ne' _ _) fun x hx => h ⟨x, hx⟩

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