Commit 2024-06-07 23:31 4bbafd44

View on Github →

chore(Order/Interval): use WithBot API (#13493)

Estimated changes

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Order/Interval/Basic.lean

modified theorem Interval.coe_inf

added def Interval.recBotCoe

added theorem NonemptyInterval.coe_def

Modified Mathlib/Order/Interval/Finset/Defs.lean