Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-12 12:46 aadba9b2

View on Github →

feat(order/well_founded_set): any relation is well-founded on Ø (#15266)

Estimated changes

Modified src/order/well_founded_set.lean

modified theorem set.is_pwo_empty

added theorem set.is_wf_empty

added theorem set.partially_well_ordered_on_empty

added theorem set.well_founded_on_empty