Commit 2026-10-13 18:29 a7b86a78

View on Github →

feat: add Semilattice lemmas for IsBotOneClass (#42538) These lemmas are analogous to the existing lemmas for LinearOrder + IsBotOneClass. The bot versions for Semilattices and LinearOrder also exist already.

Estimated changes

added theorem inf_one
modified theorem max_eq_one
modified theorem max_one
modified theorem min_one
added theorem one_inf
modified theorem one_max
modified theorem one_min
added theorem one_sup
added theorem sup_eq_one
added theorem sup_one