Commit 2025-09-04 14:12 04142815
View on Github →feat(Order/Lattice): Add some lattice lemmas (#27648) Adds some simp lemmas:
- inf_left_le_sup_right :
(a ⊓ b) ≤ (b ⊔ c) - inf_right_le_sup_right :
(b ⊓ a) ≤ (b ⊔ c) - inf_left_le_sup_left :
(a ⊓ b) ≤ (c ⊔ b) - inf_right_le_sup_left :
(b ⊓ a) ≤ (c ⊔ b)