orthonormalBasis_one_dim — Mathlib

English

There exists a bijection between the index set of a direct sum decomposition and Fin n in an internal direct sum setting.

Русский

Существует биекция между индексным множеством разложения в прямой сумме и Fin n в контексте внутренней прямой суммы.

LaTeX

$$def sigmaOrthonormalBasisIndexEquiv := ...$$

Lean4

/-- An orthonormal basis of `ℝ` is made either of the vector `1`, or of the vector `-1`. -/
theorem orthonormalBasis_one_dim (b : OrthonormalBasis ι ℝ ℝ) : (⇑b = fun _ => (1 : ℝ)) ∨ ⇑b = fun _ => (-1 : ℝ) :=
  by
  have : Unique ι := b.toBasis.unique
  have : b default = 1 ∨ b default = -1 :=
    by
    have : ‖b default‖ = 1 := b.orthonormal.1 _
    rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
  rw [eq_const_of_unique b]
  grind

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