Theorems · Definition · order theory

Antisymmetrization.prodEquiv

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

The antisymmetrization of a product preorder is order isomorphic to the product of antisymmetrizations.

Defined in

Mathlib.Order.Antisymmetrization

Cited by

2 results in Mathlib

Foundations

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

Assumes

PreorderPreorder