Commit 2025-02-28 07:09 2dccc4bd

View on Github →

feat: lemmas about intervals and finite intervals (#22199)

Estimated changes

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

added theorem Finset.Iic_diff_Ioc

added theorem Finset.Iic_diff_Ioc_self_of_le

added theorem Finset.Iic_disjoint_Ioc

added theorem Finset.Iic_union_Ioc_eq_Iic

added theorem Finset.image_subset_Iic_sup

added theorem Finset.subset_Iic_sup_id

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

added theorem Nat.mem_Ioc_succ'

added theorem Nat.mem_Ioc_succ

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

added theorem Set.Iic_diff_Ioc

added theorem Set.Iic_diff_Ioc_self_of_le

added theorem Set.compl_Ioc