instIsStrictlySupportedExtend — Mathlib

English

The extension of a homological complex along an embedding is strictly supported if the original is, in the sense of the extension data providing a strict support structure.

Русский

Расширение гомологического комплекса вдоль вложения обладает свойством строгой поддержки, если исходный комплекс имеет такое свойство, согласно данным расширения.

LaTeX

$$$(K\\extend e)\\,\\IsStrictlySupported\\ e$$$

Lean4

instance : (K.extend e).IsStrictlySupported e where isZero i' hi' := K.isZero_extend_X e i' hi'

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