flip_iff

Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsPullback.flip_iff

English

IsPullback is preserved under swapping the legs: IsPullback fst snd f g iff IsPullback snd fst g f.

Русский

Свойство IsPullback сохраняется при перестановке ног: IsPullback fst snd f g эквивалентно IsPullback snd fst g f.

LaTeX

$$$IsPullback\ fst\ snd\ f\ g \leftrightarrow IsPullback\ snd\ fst\ g\ f$$$

Lean4

theorem flip_iff : IsPullback fst snd f g ↔ IsPullback snd fst g f :=
  ⟨flip, flip⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru