Theorems · Definition · order theory

OrderHom.antisymmetrization

{α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        (α →o β) → (Antisymmetrization α fun x1 x2 => x1 ≤ x2) →o Antisymmetrization β fun x1 x2 => x1 ≤ x2

Turns an order homomorphism from α to β into one from Antisymmetrization α to Antisymmetrization β. Antisymmetrization is actually a functor. See Preorder_to_PartialOrder.

Defined in

Mathlib.Order.Antisymmetrization

Cited by

3 results in Mathlib

Foundations

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

Assumes

PreorderPreorder