inverse_eq — Mathlib

English

If f ∘ g = id and g ∘ f = id, then f.inverse = g.

Русский

Если $f$ и $g$ взаимно обратны, то обратная к $f$ равна $g$.

LaTeX

$$$(f \circ_L g = \mathrm{id}) \land (g \circ_L f = \mathrm{id}) \Rightarrow f^{-1} = g$$$

Lean4

theorem inverse_eq {f : M →L[R] M₂} {g : M₂ →L[R] M} (hf : f ∘L g = .id R M₂) (hg : g ∘L f = .id R M) : f.inverse = g :=
  by
  have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := rfl
  rw [this, inverse_equiv]
  rfl

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