instIsStrictlySupportedStupidTrunc

English

If K is a homological complex with embedding e, then its stupid truncation along e is strictly supported relative to e.

Русский

Если K — комплекс Гомологий с вложением e, то его грубое усечение вдоль e строго поддерживается относительно e.

LaTeX

$$$\mathrm{IsStrictlySupported}\bigl(K.\mathrm{stupidTrunc}(e),\ e\bigr)$$$

Lean4

instance : IsStrictlySupported (K.stupidTrunc e) e :=
  by
  dsimp [stupidTrunc]
  infer_instance

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