parallelepiped_eq_map — Mathlib

English

A parallelepiped built from a basis equals the image of a coordinate parallelepiped under the basis map.

Русский

Параллелепипед, построенный от базиса, равен образу параллелепипеда координатной системы под отображением базиса.

LaTeX

$$$b.parallelepiped = (\text{piIcc01})\!.map b.equivFun.symm \cdots$$$

Lean4

/-- A parallelepiped can be expressed on the standard basis. -/
theorem parallelepiped_eq_map {ι E : Type*} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E) :
    b.parallelepiped =
      (PositiveCompacts.piIcc01 ι).map b.equivFun.symm b.equivFunL.symm.continuous b.equivFunL.symm.isOpenMap :=
  by
  classical
  rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
  congr with x
  simp [Pi.single_apply]

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