parallelepiped_map — Mathlib

English

The parallelepiped of a product of bases equals the product parallelepiped.

Русский

Параллелепипед произведения базисов равен произведению параллелепипедов.

LaTeX

$$$ (v.prop\\,.w).parallelepiped = v.parallelepiped.prod w.parallelepiped $.$$

Lean4

theorem parallelepiped_map (b : Basis ι ℝ E) (e : E ≃ₗ[ℝ] F) :
    (b.map e).parallelepiped =
      b.parallelepiped.map e
        (haveI := FiniteDimensional.of_fintype_basis b
        LinearMap.continuous_of_finiteDimensional e.toLinearMap)
        (haveI := FiniteDimensional.of_fintype_basis (b.map e)
        LinearMap.isOpenMap_of_finiteDimensional _ e.surjective) :=
  PositiveCompacts.ext (image_parallelepiped e.toLinearMap _).symm

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