Commit 2024-10-07 17:59 912f72d3

View on Github →

feat(SetTheory/Ordinal/Exponential): more lemmas on Ordinal.log (#15990) We show multiple variants of opow_le_iff_le_log with slightly different assumptions.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

added theorem Ordinal.le_log_of_opow_le

added theorem Ordinal.lt_log_of_lt_opow

added theorem Ordinal.lt_opow_iff_log_lt'

added theorem Ordinal.lt_opow_of_log_lt

added theorem Ordinal.opow_eq_zero

added theorem Ordinal.opow_le_iff_le_log'

modified theorem Ordinal.opow_le_iff_le_log

added theorem Ordinal.opow_le_of_le_log