decompose_of_mem_same — Mathlib

English

In a decomposition ℳ, if x lies in the i-th component, then the i-th projection of its decomposition equals x.

Русский

В разложении ℳ, если x лежит в i-ой составляющей, то i-я компонента разложения равна x.

LaTeX

$$$$\\text{If } x\\in \\mathcal{M}_i,\\quad (\\mathrm{decompose}\\; \\mathcal{M}\\; x\\; i) = x.$$$$

Lean4

theorem decompose_of_mem_same {x : M} {i : ι} (hx : x ∈ ℳ i) : (decompose ℳ x i : M) = x := by
  rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

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