single_apply — Mathlib

English

The orthonormal basis on a single index set coincides with the standard basis: the singleton orthonormal basis equals the basis with a single canonical vector.

Русский

Ортонормированный базис на одном индексе совпадает с обычным базисом: единичный ортонормированный базис равен базису с единичным каноническим вектором.

LaTeX

$$$\text{(OrthonormalBasis.singleton } \iota \mathbf{K}).toBasis = \ Basis.singleton \iota \mathbf{K}$$$

Lean4

@[simp]
theorem single_apply (i : ι) (a : 𝕜) (j : ι) : (EuclideanSpace.single i a) j = ite (j = i) a 0 := by
  rw [EuclideanSpace.single, PiLp.toLp_apply, ← Pi.single_apply i a j]

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