Commit 2024-09-17 07:27 e4699dfe

View on Github →

feat(Order/WellFounded): Generalize StrictMono.id_le (#16706) This PR does the following:

  • We merge StrictMono.id_le with its previously existing proof for a well-founded linear order, and use the WellFoundedLT typeclass rather than having a WellFounded (· < ·) argument.
  • We rename eq_strictMono_iff_eq_range to the more idiomatic StrictMono.range_inj and golf it slightly by using Set.InjOn.
  • We prove order duals of these theorems.

Estimated changes

deleted theorem StrictMono.id_le
added theorem StrictAnti.range_inj
added theorem StrictMono.apply_le
added theorem StrictMono.id_le
added theorem StrictMono.le_apply
added theorem StrictMono.le_id
added theorem StrictMono.range_inj
modified theorem WellFounded.min_le
added theorem Ordinal.IsNormal.id_le