isZero_single_obj_X — Mathlib

English

For any j, A, i with i ≠ j, the component ((single V c j).obj A).X_i is a zero object.

Русский

Для любого j, A и i с i ≠ j соответствующий компонент ((single V c j).obj A).X_i является нулевым объектом.

LaTeX

$$$$ \forall j\,\forall A\,\forall i (i \neq j)\; \operatorname{IsZero}\big(((\text{single } V\ c\ j).\text{obj } A).X_i\big) $$$$

Lean4

theorem isZero_single_obj_X (j : ι) (A : V) (i : ι) (hi : i ≠ j) : IsZero (((single V c j).obj A).X i) :=
  by
  dsimp [single]
  rw [if_neg hi]
  exact Limits.isZero_zero V

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