orientation_isEmpty — Mathlib

English

If the index type ι is empty, the orientation of any basis equals the canonical positive orientation.

Русский

Если множество индексов ι пустое, ориентация любого базиса равна канонической положительной ориентации.

LaTeX

$$$$ b.{\\rm orientation} = {\\rm positiveOrientation} $$$$

Lean4

@[simp]
theorem orientation_isEmpty [IsEmpty ι] (b : Basis ι R M) : b.orientation = positiveOrientation :=
  by
  rw [Basis.orientation]
  congr
  exact b.det_isEmpty

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