mathlib

b19481de - feat(order/antichain): Antichains are order-connected (#18636)