Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-26 19:01 a7b92725

View on Github →

feat(order/locally_finite): finset.interval (#17939) A finset-valued version of set.interval.

Estimated changes

Modified src/data/finset/locally_finite.lean

added theorem finset.Icc_min_max

added theorem finset.Icc_subset_interval'

added theorem finset.Icc_subset_interval

added theorem finset.eq_of_mem_interval_of_mem_interval'

added theorem finset.eq_of_mem_interval_of_mem_interval

added theorem finset.interval_eq_union

added theorem finset.interval_injective_left

added theorem finset.interval_injective_right

added theorem finset.interval_of_ge

added theorem finset.interval_of_le

added theorem finset.interval_of_not_ge

added theorem finset.interval_of_not_le

added theorem finset.interval_self

added theorem finset.interval_subset_Icc

added theorem finset.interval_subset_interval

added theorem finset.interval_subset_interval_iff_le'

added theorem finset.interval_subset_interval_iff_le

added theorem finset.interval_subset_interval_iff_mem

added theorem finset.interval_subset_interval_left

added theorem finset.interval_subset_interval_right

added theorem finset.interval_subset_interval_union_interval

added theorem finset.interval_swap

added theorem finset.interval_to_dual

added theorem finset.left_mem_interval

added theorem finset.mem_interval'

added theorem finset.mem_interval_of_ge

added theorem finset.mem_interval_of_le

added theorem finset.nonempty_interval

added theorem finset.not_mem_interval_of_gt

added theorem finset.not_mem_interval_of_lt

added theorem finset.right_mem_interval

Modified src/order/locally_finite.lean

added theorem finset.coe_interval

added def finset.interval

added theorem finset.mem_interval

added theorem prod.card_interval

added theorem prod.interval_eq

added theorem prod.interval_mk_mk