linearEquivIncludeRange_toLinearMap

English

The linear equivalence corresponds to the tensor product map of the includeLeft and includeRight rangeRestrict maps.

Русский

Линейное эквивалентное отображение соответствует отображению тензорного произведения включающих диапазонов.

LaTeX

$$$(linearEquivIncludeRange R S T).toLinearMap = \\mathrm{TensorProduct.map}\\ includeLeft.toLinearMap.rangeRestrict\\ includeRight.toLinearMap.rangeRestrict$$$

Lean4

theorem linearEquivIncludeRange_toLinearMap :
    (linearEquivIncludeRange R S T).toLinearMap =
      _root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict :=
  rfl

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