chooseDecomposition — Mathlib

English

For any i and x ∈ ℳ_i, the i-th coordinate of decompose x is x, and all other coordinates are 0.

Русский

Для любого i и x ∈ ℳ_i, i-я координата decompose x равна x, а все прочие координаты равны 0.

LaTeX

$$$\forall i,\ decompose( x )_i = x \ and\ decompose(x)_j = 0\ (j\neq i)$$$

Lean4

/-- Noncomputably conjure a decomposition instance from a `DirectSum.IsInternal` proof. -/
noncomputable def chooseDecomposition (h : IsInternal ℳ) : DirectSum.Decomposition ℳ
    where
  decompose' := (Equiv.ofBijective _ h).symm
  left_inv := (Equiv.ofBijective _ h).right_inv
  right_inv := (Equiv.ofBijective _ h).left_inv

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