Commit 2022-12-15 05:01 03c0beb8

View on Github →

feat: Port Data.Set.Intervals.Basic (#1033)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Intervals/Basic.lean

added theorem IsBot.Ici_eq

added theorem IsMax.Ici_eq

added theorem IsMax.Ioi_eq

added theorem IsMin.Iic_eq

added theorem IsMin.Iio_eq

added theorem IsTop.Iic_eq

added def Set.Icc

added theorem Set.Icc_bot

added theorem Set.Icc_bot_top

added theorem Set.Icc_def

added theorem Set.Icc_diff_Ico_same

added theorem Set.Icc_diff_Ioc_same

added theorem Set.Icc_diff_Ioo_same

added theorem Set.Icc_diff_both

added theorem Set.Icc_diff_left

added theorem Set.Icc_diff_right

added theorem Set.Icc_eq_empty

added theorem Set.Icc_eq_empty_iff

added theorem Set.Icc_eq_empty_of_lt

added theorem Set.Icc_eq_singleton_iff

added theorem Set.Icc_inter_Icc

added theorem Set.Icc_inter_Icc_eq_singleton

added theorem Set.Icc_prod_Icc

added theorem Set.Icc_prod_eq

added theorem Set.Icc_self

added theorem Set.Icc_ssubset_Icc_left

added theorem Set.Icc_ssubset_Icc_right

added theorem Set.Icc_subset_Icc

added theorem Set.Icc_subset_Icc_iff

added theorem Set.Icc_subset_Icc_left

added theorem Set.Icc_subset_Icc_right

added theorem Set.Icc_subset_Icc_union_Icc

added theorem Set.Icc_subset_Icc_union_Ioc

added theorem Set.Icc_subset_Ici_iff

added theorem Set.Icc_subset_Ici_self

added theorem Set.Icc_subset_Ico_iff

added theorem Set.Icc_subset_Ico_right

added theorem Set.Icc_subset_Ico_union_Icc

added theorem Set.Icc_subset_Iic_iff

added theorem Set.Icc_subset_Iic_self

added theorem Set.Icc_subset_Iio_iff

added theorem Set.Icc_subset_Ioc_iff

added theorem Set.Icc_subset_Ioi_iff

added theorem Set.Icc_subset_Ioo

added theorem Set.Icc_subset_Ioo_iff

added theorem Set.Icc_top

added theorem Set.Icc_union_Icc'

added theorem Set.Icc_union_Icc

added theorem Set.Icc_union_Icc_eq_Icc

added theorem Set.Icc_union_Ici'

added theorem Set.Icc_union_Ici

added theorem Set.Icc_union_Ici_eq_Ici

added theorem Set.Icc_union_Ico_eq_Ico

added theorem Set.Icc_union_Ioc_eq_Icc

added theorem Set.Icc_union_Ioi_eq_Ici

added theorem Set.Icc_union_Ioo_eq_Ico

added def Set.Ici

added theorem Set.Ici_bot

added theorem Set.Ici_def

added theorem Set.Ici_diff_Ici

added theorem Set.Ici_diff_Ioi

added theorem Set.Ici_diff_Ioi_same

added theorem Set.Ici_diff_left

added theorem Set.Ici_inj

added theorem Set.Ici_injective

added theorem Set.Ici_inter_Ici

added theorem Set.Ici_inter_Iic

added theorem Set.Ici_inter_Iio

added theorem Set.Ici_prod_Ici

added theorem Set.Ici_prod_eq

added theorem Set.Ici_subset_Icc_union_Ici

added theorem Set.Ici_subset_Icc_union_Ioi

added theorem Set.Ici_subset_Ici

added theorem Set.Ici_subset_Ico_union_Ici

added theorem Set.Ici_subset_Ioi

added theorem Set.Ici_top

added def Set.Ico

added theorem Set.Ico_bot

added theorem Set.Ico_def

added theorem Set.Ico_diff_Iio

added theorem Set.Ico_diff_Ioo_same

added theorem Set.Ico_diff_left

added theorem Set.Ico_eq_Ico_iff

added theorem Set.Ico_eq_empty

added theorem Set.Ico_eq_empty_iff

added theorem Set.Ico_eq_empty_of_le

added theorem Set.Ico_insert_right

added theorem Set.Ico_inter_Ici

added theorem Set.Ico_inter_Ico

added theorem Set.Ico_inter_Iio

added theorem Set.Ico_self

added theorem Set.Ico_subset_Icc_self

added theorem Set.Ico_subset_Icc_union_Ico

added theorem Set.Ico_subset_Icc_union_Ioo

added theorem Set.Ico_subset_Ici_self

added theorem Set.Ico_subset_Ico

added theorem Set.Ico_subset_Ico_iff

added theorem Set.Ico_subset_Ico_left

added theorem Set.Ico_subset_Ico_right

added theorem Set.Ico_subset_Ico_union_Ico

added theorem Set.Ico_subset_Iio_self

added theorem Set.Ico_subset_Ioo_left

added theorem Set.Ico_union_Icc_eq_Icc

added theorem Set.Ico_union_Ici'

added theorem Set.Ico_union_Ici

added theorem Set.Ico_union_Ici_eq_Ici

added theorem Set.Ico_union_Ico'

added theorem Set.Ico_union_Ico

added theorem Set.Ico_union_Ico_eq_Ico

added theorem Set.Ico_union_right

added def Set.Iic

added theorem Set.Iic_bot

added theorem Set.Iic_def

added theorem Set.Iic_diff_Iic

added theorem Set.Iic_diff_Iio

added theorem Set.Iic_diff_Iio_same

added theorem Set.Iic_diff_right

added theorem Set.Iic_inj

added theorem Set.Iic_injective

added theorem Set.Iic_inter_Ici

added theorem Set.Iic_inter_Iic

added theorem Set.Iic_inter_Ioc_of_le

added theorem Set.Iic_inter_Ioi

added theorem Set.Iic_prod_Iic

added theorem Set.Iic_prod_eq

added theorem Set.Iic_subset_Iic

added theorem Set.Iic_subset_Iic_union_Icc

added theorem Set.Iic_subset_Iic_union_Ioc

added theorem Set.Iic_subset_Iio

added theorem Set.Iic_subset_Iio_union_Icc

added theorem Set.Iic_top

added theorem Set.Iic_union_Icc'

added theorem Set.Iic_union_Icc

added theorem Set.Iic_union_Icc_eq_Iic

added theorem Set.Iic_union_Ici

added theorem Set.Iic_union_Ici_of_le

added theorem Set.Iic_union_Ico_eq_Iio

added theorem Set.Iic_union_Ioc'

added theorem Set.Iic_union_Ioc

added theorem Set.Iic_union_Ioc_eq_Iic

added theorem Set.Iic_union_Ioi

added theorem Set.Iic_union_Ioi_of_le

added theorem Set.Iic_union_Ioo_eq_Iio

added def Set.Iio

added theorem Set.Iio_bot

added theorem Set.Iio_def

added theorem Set.Iio_diff_Iic

added theorem Set.Iio_diff_Iio

added theorem Set.Iio_inj

added theorem Set.Iio_injective

added theorem Set.Iio_insert

added theorem Set.Iio_inter_Ici

added theorem Set.Iio_inter_Iio

added theorem Set.Iio_inter_Ioi

added theorem Set.Iio_ssubset_Iic_self

added theorem Set.Iio_subset_Iic

added theorem Set.Iio_subset_Iic_iff

added theorem Set.Iio_subset_Iic_self

added theorem Set.Iio_subset_Iic_union_Ico

added theorem Set.Iio_subset_Iic_union_Ioo

added theorem Set.Iio_subset_Iio

added theorem Set.Iio_subset_Iio_iff

added theorem Set.Iio_subset_Iio_union_Ico

added theorem Set.Iio_union_Icc_eq_Iic

added theorem Set.Iio_union_Ici

added theorem Set.Iio_union_Ici_of_le

added theorem Set.Iio_union_Ico'

added theorem Set.Iio_union_Ico

added theorem Set.Iio_union_Ico_eq_Iio

added theorem Set.Iio_union_Ioi

added theorem Set.Iio_union_Ioi_of_lt

added theorem Set.Iio_union_Ioo'

added theorem Set.Iio_union_Ioo

added theorem Set.Iio_union_right

added def Set.Ioc

added theorem Set.Ioc_def

added theorem Set.Ioc_diff_Iic

added theorem Set.Ioc_diff_Ioi

added theorem Set.Ioc_diff_Ioo_same

added theorem Set.Ioc_diff_right

added theorem Set.Ioc_eq_empty

added theorem Set.Ioc_eq_empty_iff

added theorem Set.Ioc_eq_empty_of_le

added theorem Set.Ioc_insert_left

added theorem Set.Ioc_inter_Iic

added theorem Set.Ioc_inter_Ioc

added theorem Set.Ioc_inter_Ioi

added theorem Set.Ioc_inter_Ioo_of_left_lt

added theorem Set.Ioc_inter_Ioo_of_right_le

added theorem Set.Ioc_self

added theorem Set.Ioc_subset_Icc_self

added theorem Set.Ioc_subset_Iic_self

added theorem Set.Ioc_subset_Ioc

added theorem Set.Ioc_subset_Ioc_iff

added theorem Set.Ioc_subset_Ioc_left

added theorem Set.Ioc_subset_Ioc_right

added theorem Set.Ioc_subset_Ioc_union_Icc

added theorem Set.Ioc_subset_Ioc_union_Ioc

added theorem Set.Ioc_subset_Ioi_self

added theorem Set.Ioc_subset_Ioo_right

added theorem Set.Ioc_subset_Ioo_union_Icc

added theorem Set.Ioc_top

added theorem Set.Ioc_union_Icc_eq_Ioc

added theorem Set.Ioc_union_Ici_eq_Ioi

added theorem Set.Ioc_union_Ico_eq_Ioo

added theorem Set.Ioc_union_Ioc'

added theorem Set.Ioc_union_Ioc

added theorem Set.Ioc_union_Ioc_eq_Ioc

added theorem Set.Ioc_union_Ioc_left

added theorem Set.Ioc_union_Ioc_right

added theorem Set.Ioc_union_Ioc_symm

added theorem Set.Ioc_union_Ioc_union_Ioc_cycle

added theorem Set.Ioc_union_Ioi'

added theorem Set.Ioc_union_Ioi

added theorem Set.Ioc_union_Ioi_eq_Ioi

added theorem Set.Ioc_union_Ioo_eq_Ioo

added theorem Set.Ioc_union_left

added def Set.Ioi

added theorem Set.Ioi_def

added theorem Set.Ioi_diff_Ici

added theorem Set.Ioi_diff_Ioi

added theorem Set.Ioi_inj

added theorem Set.Ioi_injective

added theorem Set.Ioi_insert

added theorem Set.Ioi_inter_Iic

added theorem Set.Ioi_inter_Iio

added theorem Set.Ioi_inter_Ioi

added theorem Set.Ioi_ssubset_Ici_self

added theorem Set.Ioi_subset_Ici

added theorem Set.Ioi_subset_Ici_iff

added theorem Set.Ioi_subset_Ici_self

added theorem Set.Ioi_subset_Ioc_union_Ici

added theorem Set.Ioi_subset_Ioc_union_Ioi

added theorem Set.Ioi_subset_Ioi

added theorem Set.Ioi_subset_Ioi_iff

added theorem Set.Ioi_subset_Ioo_union_Ici

added theorem Set.Ioi_top

added theorem Set.Ioi_union_left

added def Set.Ioo

added theorem Set.Ioo_def

added theorem Set.Ioo_eq_empty

added theorem Set.Ioo_eq_empty_iff

added theorem Set.Ioo_eq_empty_of_le

added theorem Set.Ioo_insert_left

added theorem Set.Ioo_insert_right

added theorem Set.Ioo_inter_Ioc_of_left_le

added theorem Set.Ioo_inter_Ioc_of_right_lt

added theorem Set.Ioo_inter_Ioo

added theorem Set.Ioo_self

added theorem Set.Ioo_subset_Icc_self

added theorem Set.Ioo_subset_Ico_self

added theorem Set.Ioo_subset_Iio_self

added theorem Set.Ioo_subset_Ioc_self

added theorem Set.Ioo_subset_Ioc_union_Ico

added theorem Set.Ioo_subset_Ioc_union_Ioo

added theorem Set.Ioo_subset_Ioi_self

added theorem Set.Ioo_subset_Ioo

added theorem Set.Ioo_subset_Ioo_iff

added theorem Set.Ioo_subset_Ioo_left

added theorem Set.Ioo_subset_Ioo_right

added theorem Set.Ioo_subset_Ioo_union_Ico

added theorem Set.Ioo_union_Icc_eq_Ioc

added theorem Set.Ioo_union_Ici_eq_Ioi

added theorem Set.Ioo_union_Ico_eq_Ioo

added theorem Set.Ioo_union_Ioi'

added theorem Set.Ioo_union_Ioi

added theorem Set.Ioo_union_Ioo'

added theorem Set.Ioo_union_Ioo

added theorem Set.Ioo_union_left

added theorem Set.Ioo_union_right

added theorem Set.compl_Ici

added theorem Set.compl_Iic

added theorem Set.compl_Iio

added theorem Set.compl_Ioi

added theorem Set.dual_Icc

added theorem Set.dual_Ici

added theorem Set.dual_Ico

added theorem Set.dual_Iic

added theorem Set.dual_Iio

added theorem Set.dual_Ioc

added theorem Set.dual_Ioi

added theorem Set.dual_Ioo

added theorem Set.eq_endpoints_or_mem_Ioo_of_mem_Icc

added theorem Set.eq_left_or_mem_Ioo_of_mem_Ico

added theorem Set.eq_right_or_mem_Ioo_of_mem_Ioc

added theorem Set.left_mem_Icc

added theorem Set.left_mem_Ici

added theorem Set.left_mem_Ico

added theorem Set.left_mem_Ioc

added theorem Set.left_mem_Ioo

added theorem Set.mem_Icc

added theorem Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset

added theorem Set.mem_Icc_of_Ico

added theorem Set.mem_Icc_of_Ioc

added theorem Set.mem_Icc_of_Ioo

added theorem Set.mem_Ici

added theorem Set.mem_Ici_Ioi_of_subset_of_subset

added theorem Set.mem_Ici_of_Ioi

added theorem Set.mem_Ico

added theorem Set.mem_Ico_of_Ioo

added theorem Set.mem_Iic

added theorem Set.mem_Iic_Iio_of_subset_of_subset

added theorem Set.mem_Iic_of_Iio

added theorem Set.mem_Iio

added theorem Set.mem_Ioc

added theorem Set.mem_Ioc_of_Ioo

added theorem Set.mem_Ioi

added theorem Set.mem_Ioo

added theorem Set.nonempty_Icc

added theorem Set.nonempty_Icc_subtype

added theorem Set.nonempty_Ici

added theorem Set.nonempty_Ico

added theorem Set.nonempty_Ico_subtype

added theorem Set.nonempty_Iic

added theorem Set.nonempty_Iio

added theorem Set.nonempty_Ioc

added theorem Set.nonempty_Ioc_subtype

added theorem Set.nonempty_Ioi

added theorem Set.nonempty_Ioo

added theorem Set.nonempty_Ioo_subtype

added theorem Set.not_mem_Icc_of_gt

added theorem Set.not_mem_Icc_of_lt

added theorem Set.not_mem_Ici

added theorem Set.not_mem_Ico_of_ge

added theorem Set.not_mem_Ico_of_lt

added theorem Set.not_mem_Iic

added theorem Set.not_mem_Iio

added theorem Set.not_mem_Iio_self

added theorem Set.not_mem_Ioc_of_gt

added theorem Set.not_mem_Ioc_of_le

added theorem Set.not_mem_Ioi

added theorem Set.not_mem_Ioi_self

added theorem Set.not_mem_Ioo_of_ge

added theorem Set.not_mem_Ioo_of_le

added theorem Set.right_mem_Icc

added theorem Set.right_mem_Ico

added theorem Set.right_mem_Iic

added theorem Set.right_mem_Ioc

added theorem Set.right_mem_Ioo

Modified Mathlib/Order/MinMax.lean