Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-11 04:06 2c53e5ee

View on Github →

chore(order/well_founded): move to a file (#4568) I want to use order/rel_classes before data/set/basic.

Estimated changes

Modified archive/imo/imo1988_q6.lean

Modified src/data/fintype/basic.lean

Modified src/order/lattice.lean

added theorem lt_sup_iff

Modified src/order/pilex.lean

Modified src/order/rel_classes.lean

deleted theorem well_founded.eq_iff_not_lt_of_le

deleted theorem well_founded.has_min

deleted theorem well_founded.min_mem

deleted theorem well_founded.not_lt_min

deleted theorem well_founded.well_founded_iff_has_max'

deleted theorem well_founded.well_founded_iff_has_min'

deleted theorem well_founded.well_founded_iff_has_min

Created src/order/well_founded.lean

added theorem well_founded.eq_iff_not_lt_of_le

added theorem well_founded.has_min

added theorem well_founded.min_mem

added theorem well_founded.not_lt_min

added theorem well_founded.well_founded_iff_has_max'

added theorem well_founded.well_founded_iff_has_min'

added theorem well_founded.well_founded_iff_has_min