left_adjoint_hasLift_iff — Mathlib

English

A left adjoint square has a lifting if and only if the original square has a lifting.

Русский

Левый сопряжённый квадрат имеет подъем тогда и только тогда, когда исходный квадрат имеет подъем.

LaTeX

$$$$ HasLift( sq.left\\_adjoint adj ) \\iff HasLift( sq ) $$$$

Lean4

/-- A (left) adjoint square has a lifting if and only if the original square has a lifting. -/
theorem left_adjoint_hasLift_iff : HasLift (sq.left_adjoint adj) ↔ HasLift sq :=
  by
  simp only [HasLift.iff]
  exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm

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