Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-14 19:58 2c84c2c5

View on Github →

feat(order/well_founded_set): prod.lex is well-founded (#18665)

Estimated changes

Modified src/order/well_founded.lean

added theorem well_founded.mono

added theorem well_founded.on_fun

Modified src/order/well_founded_set.lean

added theorem set.well_founded_on.mono'

added theorem set.well_founded_on.prod_lex_of_well_founded_on_fiber

added theorem set.well_founded_on.sigma_lex_of_well_founded_on_fiber

added theorem set.well_founded_on_image

added theorem set.well_founded_on_range

added theorem set.well_founded_on_univ

added theorem well_founded.prod_lex_of_well_founded_on_fiber

added theorem well_founded.sigma_lex_of_well_founded_on_fiber

added theorem well_founded.well_founded_on