inverse_comp_apply_of_left — Mathlib

English

If g is invertible, then (g ∘ f).inverse = f.inverse ∘ g.inverse.

Русский

Если $g$ обратимо, то обратная к $g \circ f$ равна $f^{-1} \circ g^{-1}$.

LaTeX

$$$\text{If } g^{-1} \text{ exists},\; (g \circ_L f).inverse = f.inverse \circ_L g.inverse$$$

Lean4

theorem inverse_comp_apply_of_left {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃} (hg : g.IsInvertible) :
    (g ∘L f).inverse v = f.inverse (g.inverse v) := by
  simp only [hg.inverse_comp_of_left, coe_comp', Function.comp_apply]

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