Theorems · Theorem · order theory

Antisymmetrization.induction_on

∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] {p : Antisymmetrization α r → Prop}
  (a : Antisymmetrization α r), (∀ (a : α), p (toAntisymmetrization r a)) → p a

Defined in

Mathlib.Order.Antisymmetrization

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

IsPreorder