Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 16:51 9a2e5c8b

View on Github →

fix(order/basic): fix subtype.linear_order (#15056) This makes subtype.lattice definitionally equal to linear_order.to_lattice, after unfolding some (which?) semireducible definitions.

  • Rewrite linear_order.lift to allow custom max and min fields. Move the old definition to linear_order.lift'.
  • Use the new linear_order.lift to fix a non-defeq diamond on subtype _.
  • Use the new linear_order.lift in various function.injective.linear_* definitions.

Estimated changes

modified def linear_order.lift
added theorem max_rec'
added theorem max_rec
added theorem min_rec'
added theorem min_rec
deleted theorem max_rec'
deleted theorem max_rec
deleted theorem min_rec'
deleted theorem min_rec