inverse_of_not_isInvertible — Mathlib

English

If a continuous linear map is not invertible, its inverse is defined to be the zero map.

Русский

Если непрерывно-линейное отображение не обратимо, его обратное определяется как нулевое отображение.

LaTeX

$$$ f. inverse = 0 \quad \text{when } \neg f.IsInvertible $$$

Lean4

/-- By definition, if `f` is not invertible then `inverse f = 0`. -/
@[simp]
theorem inverse_of_not_isInvertible {f : M →L[R] M₂} (hf : ¬f.IsInvertible) : f.inverse = 0 :=
  dif_neg hf

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