of_inverse — Mathlib

English

If f ∘ g = id and g ∘ f = id, then f is invertible.

Русский

Если $f \circ g = \mathrm{id}$ и $g \circ f = \mathrm{id}$, то $f$ обратимо.

LaTeX

$$$(f \circ_L g = \mathrm{id}) \land (g \circ_L f = \mathrm{id}) \Rightarrow f \text{ is invertible}$$$

Lean4

theorem of_inverse {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.IsInvertible :=
  ⟨ContinuousLinearEquiv.equivOfInverse' _ _ hf hg, rfl⟩

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