update_comp_eq_of_injective' — Mathlib

English

If g : α → β is updated at i and then composed with f, this equals updating the composed g along f at i.

Русский

Если g обновляется в точке i и затем композиционно применяется к f, то это равно обновлению композиции g по f в точке i.

LaTeX

$$$(\\lambda j, update\\ g\\ (f i)\\ a\\ (f j)) = (\\lambda j, update (\\lambda k, g( f k)) i a j)$$$

Lean4

theorem update_comp_eq_of_injective' (g : ∀ a, β a) {f : α' → α} (hf : Function.Injective f) (i : α') (a : β (f i)) :
    (fun j ↦ update g (f i) a (f j)) = update (fun i ↦ g (f i)) i a :=
  eq_update_iff.2 ⟨update_self .., fun _ hj ↦ update_of_ne (hf.ne hj) _ _⟩

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