decompose_of_mem_ne — Mathlib

English

If x lies in component ℳ_i and i ≠ j, the j-th coordinate of decompose x is zero.

Русский

Если x лежит в компоненте i и i ≠ j, j-я координата x в разложении равна нулю.

LaTeX

$$$x\in \mathcal{M}_i \land i \neq j \quad\Rightarrow\quad (\mathrm{decompose}_{\mathcal{M}}(x))_j = 0$$$

Lean4

theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j) : (decompose ℳ x j : M) = 0 := by
  rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]

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