flip — Mathlib

English

Flipping a bicartesian square yields another bicartesian square with the legs exchanged: If p is a BicartesianSq f g h i, then flip p is BicartesianSq g f i h.

Русский

Поменяв местами стороны бикартезианского квадрата, получаем другой бикартезианский квадрат: если p — BicartesianSq f g h i, то flip p — BicartesianSq g f i h.

LaTeX

$$$ \\operatorname{flip}(\\operatorname{BicartesianSq}(f,g,h,i)) = \\operatorname{BicartesianSq}(g,f,i,h) $$$

Lean4

theorem flip (p : BicartesianSq f g h i) : BicartesianSq g f i h :=
  of_isPullback_isPushout p.toIsPullback.flip p.toIsPushout.flip

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