Commit 2026-05-12 09:49 a06a909a

View on Github →

feat: min and max theorems for IsBotZeroClass (#39057) We also remove a redundant ZeroLEOneClass Ordinal instance (which can now be inferred via CanonicallyOrderedAdd → IsBotZeroClass → ZeroLEOneClass).

Estimated changes

added theorem max_eq_one
added theorem max_one
added theorem min_eq_one
modified theorem min_one
added theorem one_max
modified theorem one_min
modified theorem ENNReal.max_eq_zero_iff
modified theorem ENNReal.min_eq_zero_iff
deleted theorem Ordinal.max_eq_zero
modified theorem Metric.ediam_pair
modified theorem Metric.ediam_triple