instHasTotalFlip_1 — Mathlib

English

There is an instance carrying the fact that the flipped bicomplex also has a total structure whenever the original does.

Русский

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

LaTeX

$$$K.flip.flip.HasTotal\ c$$$

Lean4

instance : K.flip.flip.HasTotal c :=
  (inferInstance : K.HasTotal c)

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