Commit 2022-12-16 12:00 36752994

View on Github →

feat: port Order.LatticeIntervals (#1070) Lots of renames, but easy. I've added names for all instances

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/LatticeIntervals.lean

added theorem Set.Ici.coe_bot

added theorem Set.Ici.coe_top

added theorem Set.Iic.coe_bot

added theorem Set.Iic.coe_top