Commit 2026-08-06 01:28 7bd8067d

View on Github →

chore(Order/Bounds/Basic): use to_dual more (#42362)

Estimated changes

modified theorem bddAbove_Icc
modified theorem bddAbove_Ico
deleted theorem bddAbove_Ioc
modified theorem bddAbove_Ioo
deleted theorem bddBelow_Icc
modified theorem bddBelow_Ico
deleted theorem bddBelow_Ioc
deleted theorem bddBelow_Ioo
deleted theorem isGLB_Icc
deleted theorem isGLB_Ico
deleted theorem isLUB_Ico
deleted theorem isLUB_Ioo
deleted theorem isLeast_Icc
deleted theorem isLeast_Ico
deleted theorem lowerBounds_Icc
deleted theorem lowerBounds_Ico
deleted theorem upperBounds_Ico
deleted theorem upperBounds_Ioo