Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.well_founded_on_empty

Modification history

2022-07-12 12:46

src/order/well_founded_set.lean

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

Added set.well_founded_on_empty View on Github →