mathlib3
1c56a8de - feat(order/well_founded_set): Antichains in a partial well order are finite (#11286)

Commit

3 years ago

feat(order/well_founded_set): Antichains in a partial well order are finite (#11286) and when the relation is reflexive and symmetric, it's actually an equivalent condition.

Author

YaelDillies

Parents

0d5bfd7b

mathlib3 1c56a8de - feat(order/well_founded_set): Antichains in a partial well order are finite (#11286)

mathlib3
1c56a8de - feat(order/well_founded_set): Antichains in a partial well order are finite (#11286)