Commit 2026-05-27 17:34 4b5956c1

View on Github →

chore: deprecate duplicate theorems on ENat (#39854) These exist more generally in the setting of SuccAddOrder.

Estimated changes

modified theorem Order.Iic_one
modified theorem Order.Iic_two
modified theorem Order.Iio_one
modified theorem Order.Iio_two
modified theorem Order.le_one_iff
modified theorem Order.le_two_iff
modified theorem Order.lt_one_iff
modified theorem Order.lt_two_iff
added theorem ENat.lt_two_iff
deleted theorem ENat.one_le_iff_ne_zero
added theorem ENat.epow_pos
modified theorem Set.encard_lt_one
modified theorem Cardinal.toENat_lt_one
modified theorem ENat.card_fun
modified theorem ENat.card_pos_iff_nonempty