prop_ihom — Mathlib

English

If P is MonoidalClosed and IsMonoidalClosed, then P preserves the ihom construction: P((ihom X).obj Y) holds when P X and P Y hold.

Русский

Если P — монадо-замкнутое и IsMonoidalClosed, тогда P сохраняет конструкцию ihom: P((ihom X).obj Y) верно при верности P X и P Y.

LaTeX

$$$P((ihom\\; X).\\mathrm{obj}\\; Y)$ under MonoidalClosed and P.IsMonoidalClosed$$

Lean4

theorem prop_ihom (P : ObjectProperty C) [MonoidalClosed C] [P.IsMonoidalClosed] {X Y : C} (hX : P X) (hY : P Y) :
    P ((ihom X).obj Y) :=
  IsMonoidalClosed.prop_ihom _ _ hX hY

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