Commit 2022-12-13 21:24 5dc56e9b

View on Github →

feat port: Order.WellFounded (#970) 1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e Main change here was to remove some @[simp] attributes because simp apparently could not prove the lemma Y by simp [Y].

Estimated changes

added theorem Acc.induction_bot'
added theorem Acc.induction_bot
added theorem Function.argminOn_le
added theorem Function.argminOn_mem
added theorem Function.argmin_le
added theorem Function.not_lt_argmin
added theorem WellFounded.has_min
added theorem WellFounded.min_le
added theorem WellFounded.min_mem
added theorem WellFounded.not_lt_min