iff

Mathlib.CategoryTheory.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CommSq.HasLift.iff

English

HasLift sq is equivalent to Nonempty sq.LiftStruct.

Русский

HasLift sq эквивалентен тому, что sq.LiftStruct не пуст.

LaTeX

$$$HasLift\ sq \leftrightarrow Nonempty\ (sq\.LiftStruct)$$$

Lean4

theorem iff : HasLift sq ↔ Nonempty sq.LiftStruct := by
  constructor
  exacts [fun h => h.exists_lift, fun h => mk h]

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

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

Разделы

Аффилиация

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