Theorems · Definition · order theory

Frm.ofHom

{X Y : Type u} →
  [inst : Order.Frame X] →
    [inst_1 : Order.Frame Y] → FrameHom X Y → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })

Typecheck a FrameHom as a morphism in Frm.

Defined in

Mathlib.Order.Category.Frm

Cited by

9 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

Order.FrameOrder.Frame