flip_hasTotal_iff — Mathlib

English

The total structure exists for the flipped bicomplex if and only if it exists for the original one.

Русский

Существование полной структуры для перевернутого биокомплекса эквивалентно существованию для исходного.

LaTeX

$$$K.flip.HasTotal c \; \iff \; K.HasTotal c$$$

Lean4

theorem flip_hasTotal_iff : K.flip.HasTotal c ↔ K.HasTotal c :=
  by
  constructor
  · intro
    change K.flip.flip.HasTotal c
    have := TotalComplexShapeSymmetry.symmetry c₁ c₂ c
    infer_instance
  · intro
    infer_instance

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