isStrictlySupported_op_iff — Mathlib

English

Let K be a homological complex and e an embedding. Then K is strictly supported with respect to e if and only if its opposite K^{op} is strictly supported with respect to e^{op}.

Русский

Пусть K — гомологический комплекс и e — вложение. Тогда K строго поддержан относительно e тогда и только тогда, когда противоположный комплекс K^{op} строго поддержан относительно противоположного вложения e^{op}.

LaTeX

$$$K^{op}.IsStrictlySupported(e^{op}) \iff K.IsStrictlySupported(e)$$$

Lean4

@[simp]
theorem isStrictlySupported_op_iff : K.op.IsStrictlySupported e.op ↔ K.IsStrictlySupported e :=
  ⟨(fun _ ↦ ⟨fun i' hi' ↦ (K.op.isZero_X_of_isStrictlySupported e.op i' hi').unop⟩),
    (fun _ ↦ ⟨fun i' hi' ↦ (K.isZero_X_of_isStrictlySupported e i' hi').op⟩)⟩

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