obj_X — Mathlib

English

The nth level of the alternating face map complex equals the nth level of X: (AlternatingFaceMapComplex.obj X).X n = X_{⟨n⟩}.

Русский

Числовой уровень n чередующегося лицевого отображения комплекса равен n-му уровню X: (Obj X).X n = X_{⟨n⟩}.

LaTeX

$$$((\mathrm{AlternatingFaceMapComplex}.obj X).X n) = X_{\langle n \rangle}$$$

Lean4

@[simp]
theorem obj_X (X : SimplicialObject C) (n : ℕ) : (AlternatingFaceMapComplex.obj X).X n = X _⦋n⦌ :=
  rfl

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