Commit 2026-08-12 12:06 c8cc5952

View on Github →

chore(Order/Defs/LinearOrder): move fundamental lemmas (#42373) Also simplifies the proofs of several lemmas. This prepares for #35881.

Estimated changes

modified theorem le_min
modified theorem lt_min
modified theorem max_def'
added theorem max_le_iff
added theorem max_lt_iff
modified theorem min_assoc
modified theorem min_def'
added theorem min_le_iff
modified theorem min_le_left
modified theorem min_le_right
added theorem min_lt_iff
deleted theorem le_max_iff
deleted theorem le_min_iff
deleted theorem lt_max_iff
deleted theorem lt_min_iff