instIsStrictlySupportedOppositeOpOp

English

If a complex K is strictly supported with respect to an embedding e, then its opposite K^{op} is strictly supported with respect to e^{op}.

Русский

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

LaTeX

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

Lean4

instance [K.IsStrictlySupported e] : K.op.IsStrictlySupported e.op :=
  by
  rw [isStrictlySupported_op_iff]
  infer_instance

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