Commit 2023-01-02 22:12 e3aa1bf5

View on Github →

feat: port Order.SuccPred.IntervalSucc (#1301)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SuccPred/IntervalSucc.lean

added theorem Antitone.pairwise_disjoint_on_Ico_pred

added theorem Antitone.pairwise_disjoint_on_Ico_succ

added theorem Antitone.pairwise_disjoint_on_Ioc_pred

added theorem Antitone.pairwise_disjoint_on_Ioc_succ

added theorem Antitone.pairwise_disjoint_on_Ioo_pred

added theorem Antitone.pairwise_disjoint_on_Ioo_succ

added theorem Monotone.bunionᵢ_Ico_Ioc_map_succ

added theorem Monotone.pairwise_disjoint_on_Ico_pred

added theorem Monotone.pairwise_disjoint_on_Ico_succ

added theorem Monotone.pairwise_disjoint_on_Ioc_pred

added theorem Monotone.pairwise_disjoint_on_Ioc_succ

added theorem Monotone.pairwise_disjoint_on_Ioo_pred

added theorem Monotone.pairwise_disjoint_on_Ioo_succ