Commit 2024-11-14 05:52 06d57536

View on Github →

chore(Order/Interval/Finset): fix namespace of Ixx_orderDual_def (#18999) I just introduced these names two days ago

Estimated changes

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

added theorem Finset.Icc_orderDual_def

added theorem Finset.Ico_orderDual_def

added theorem Finset.Ioc_orderDual_def

added theorem Finset.Ioo_orderDual_def

deleted theorem Icc_orderDual_def

deleted theorem Ico_orderDual_def

deleted theorem Ioc_orderDual_def

deleted theorem Ioo_orderDual_def