instIsIsoιTruncLEOfIsStrictlySupported

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instIsIsoιTruncLEOfIsStrictlySupported

English

If K is strictly supported with respect to e, then K.ιTruncLE e is an isomorphism.

Русский

Если K строго поддержано относительно e, то K.ιTruncLE e является изоморфизмом.

LaTeX

$$$ IsIso \big(K.ιTruncLE e\big)$$$

Lean4

instance [K.IsStrictlySupported e] : IsIso (K.ιTruncLE e) :=
  inferInstanceAs (IsIso ((unopFunctor C c'.symm).map (K.op.πTruncGE e.op).op))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru