Commit 2024-11-05 13:02 060720eb

View on Github →

chore(Order/Intervals/Set): move some defs to a new file (#17950)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Submonoid.lean

Modified Mathlib/Algebra/Order/Monoid/Submonoid.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Order.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Int/Lemmas.lean

Modified Mathlib/Data/Nat/Log.lean

Modified Mathlib/Order/Fin/Tuple.lean

Modified Mathlib/Order/Hom/Set.lean

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

deleted def Set.Icc

deleted theorem Set.Icc_def

deleted def Set.Ici

deleted theorem Set.Ici_def

deleted def Set.Ico

deleted theorem Set.Ico_def

deleted def Set.Iic

deleted theorem Set.Iic_def

deleted def Set.Iio

deleted theorem Set.Iio_def

deleted def Set.Ioc

deleted theorem Set.Ioc_def

deleted def Set.Ioi

deleted theorem Set.Ioi_def

deleted def Set.Ioo

deleted theorem Set.Ioo_def

deleted theorem Set.mem_Icc

deleted theorem Set.mem_Ici

deleted theorem Set.mem_Ico

deleted theorem Set.mem_Iic

deleted theorem Set.mem_Iio

deleted theorem Set.mem_Ioc

deleted theorem Set.mem_Ioi

deleted theorem Set.mem_Ioo

Created Mathlib/Order/Interval/Set/Defs.lean

added def Set.Icc

added theorem Set.Icc_def

added def Set.Ici

added theorem Set.Ici_def

added def Set.Ico

added theorem Set.Ico_def

added def Set.Iic

added theorem Set.Iic_def

added def Set.Iio

added theorem Set.Iio_def

added def Set.Ioc

added theorem Set.Ioc_def

added def Set.Ioi

added theorem Set.Ioi_def

added def Set.Ioo

added theorem Set.Ioo_def

added theorem Set.mem_Icc

added theorem Set.mem_Ici

added theorem Set.mem_Ico

added theorem Set.mem_Iic

added theorem Set.mem_Iio

added theorem Set.mem_Ioc

added theorem Set.mem_Ioi

added theorem Set.mem_Ioo

Modified Mathlib/Order/Interval/Set/OrdConnected.lean