basisFun_equivFun — Mathlib

English

The basisFun basis is canonically equivalent to the identity function on the function space; i.e., its equivalence to the identity is given by refl.

Русский

Базис basisFun канонически эквивалентен тождественному отображению на пространство функций; эквивалентность равна тождественному отображению.

LaTeX

$$$\text{basisFun_equivFun } : (\Pi.basisFun R η).equivFun = \text{LinearEquiv.refl } _ _$$$

Lean4

@[simp]
theorem basisFun_equivFun : (Pi.basisFun R η).equivFun = LinearEquiv.refl _ _ :=
  Basis.equivFun_ofEquivFun _

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