Theorems · Theorem · order theory

OrderEmbedding.ofAntisymmetrization_apply

∀ (α : Type u_1) [inst : Preorder α] (a : Antisymmetrization α fun x1 x2 => x1 ≤ x2),
  (OrderEmbedding.ofAntisymmetrization α) a = ofAntisymmetrization (fun x1 x2 => x1 ≤ x2) a

Defined in

Mathlib.Order.Antisymmetrization

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Preorder