acyclic_truncLE_iff_isSupportedOutside

English

(K.truncLE e) is acyclic iff K.IsSupportedOutside e.

Русский

(K.truncLE e) ацикличен тогда и только тогда, когда K.IsSupportedOutside e истинно.

LaTeX

$$$ (K.truncLE e).Acyclic \iff K.IsSupportedOutside e $$$

Lean4

theorem acyclic_truncLE_iff_isSupportedOutside : (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e :=
  by
  rw [← acyclic_op_iff, ← isSupportedOutside_op_iff]
  exact K.op.acyclic_truncGE_iff_isSupportedOutside e.op

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