iff_unop — Mathlib

English

HasLiftingProperty i p is equivalent to the existence, for all φ between Arrow.mk i and Arrow.mk p, of a LiftStruct.

Русский

HasLiftingProperty i p эквивалентно существованию для каждого φ между Arrow.mk i и Arrow.mk p подъёмной структуры.

LaTeX

$$$$ HasLiftingProperty\, i\, p \\iff \\forall \\phi : Arrow.mk\, i \\to Arrow.mk\, p, \\operatorname{Nonempty}(LiftStruct(\\phi)) $$$$

Lean4

theorem iff_unop {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty p.unop i.unop :=
  ⟨unop, op⟩

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