isInvertible_equiv — Mathlib

English

A continuous linear equivalence automatically satisfies invertibility of its underlying linear map.

Русский

Непрерывно-линейное эквивалентное отображение автоматически удовлетворяет обратимости своей линейной карты.

LaTeX

$$$ f \in \text{ContinuousLinearEquiv} \Rightarrow f.toContinuousLinearMap.IsInvertible $$$

Lean4

@[simp]
theorem isInvertible_equiv {f : M ≃L[R] M₂} : IsInvertible (f : M →L[R] M₂) :=
  ⟨f, rfl⟩

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