Commit 2023-01-25 11:55 459f352b

View on Github →

Refactor: reduce imports of Data.Set.Finite (#1738) Partial forward-port of leanprover-community/mathlib#18245

Estimated changes

Modified Mathlib/Data/Set/Finite.lean

added theorem Finite.of_forall_not_lt_lt

added theorem Set.finite_diff_unionᵢ_Ioo'

added theorem Set.finite_diff_unionᵢ_Ioo

deleted theorem Set.finite_of_forall_between_eq_endpoints

added theorem Set.finite_of_forall_not_lt_lt

Modified Mathlib/Order/Basic.lean

added theorem eq_or_eq_or_eq_of_forall_not_lt_lt