Commit 2026-01-29 14:55 c07c0a65

View on Github →

chore(Order/Bounds/Basic): rename lub_Iio_le to le_of_isLUB_Iio (#34080) Rename lub_Iio_le, as was requested in #33760

Estimated changes

added theorem le_of_isLUB_Iio
deleted theorem lub_Iio_le