toUnit — Mathlib

English

From a continuous linear equivalence f one obtains a unit in the endomorphism algebra by taking f and its inverse as a pair.

Русский

Из непрерывного линейного эквивалента f получают единичу в алгебре концевых отображений за счёт пары f и её обратного.

LaTeX

$$$toUnit(f)\\in (M \\toL[R] M)^{\\times}$$$

Lean4

/-- A continuous equivalence from `M` to itself determines an invertible continuous linear map. -/
def toUnit (f : M ≃L[R] M) : (M →L[R] M)ˣ where
  val := f
  inv := f.symm
  val_inv := by
    ext
    simp
  inv_val := by
    ext
    simp

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