comp — Mathlib

English

If g and f are invertible, then the composition g ∘ f is invertible.

Русский

Если g и f обратимы, то композиция g ∘ f обратимая.

LaTeX

$$$\text{If } g: M_2 \to_L[R] M_3 \text{ and } f: M \to_L[R] M_2 \text{ are invertible, then } (g \circ_L f) \text{ is invertible.}$$$

Lean4

theorem comp {g : M₂ →L[R] M₃} {f : M →L[R] M₂} (hg : g.IsInvertible) (hf : f.IsInvertible) : (g ∘L f).IsInvertible :=
  by
  rcases hg with ⟨N, rfl⟩
  rcases hf with ⟨M, rfl⟩
  exact ⟨M.trans N, rfl⟩

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