mathlib

00d9016e - feat(order/antichain): Weak antichains (#17075)

feat(order/antichain): Weak antichains (#17075) Define weak antichains, which are sets in `Π i, α i` such that no two elements are "comparable" where "comparable" here means `∀ i, a i < b i`