update_inv — Mathlib

English

Updating the inverse coordinatewise commutes with taking inverses: update f1⁻¹ at i by x₁⁻¹ equals (update f1 at i by x₁)⁻¹.

Русский

Обновление обратного по координатам согласуется с взятием обратного: обновление f1⁻¹ в i на x₁⁻¹ равно обратному обновлению f1 в i на x₁.

LaTeX

$$$\mathrm{update}\, (f_1)\; i\; x_1)^{-1} = (\mathrm{update}\, f_1\; i\; x_1)^{-1}$$$

Lean4

@[to_additive]
theorem update_inv [∀ i, Inv (f i)] [DecidableEq I] (f₁ : ∀ i, f i) (i : I) (x₁ : f i) :
    update f₁⁻¹ i x₁⁻¹ = (update f₁ i x₁)⁻¹ :=
  funext fun j => (apply_update (fun _ => Inv.inv) f₁ i x₁ j).symm

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