Commit 2022-12-20 05:15 e90dd14f

View on Github →

feat: port Data.Set.Intervals.UnorderedInterval (#1062)

Estimated changes

Modified Mathlib.lean

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

added theorem Set.Icc_min_max

added theorem Set.Icc_subset_interval'

added theorem Set.Icc_subset_interval

added theorem Set.Ioc_subset_intervalOC'

added theorem Set.Ioc_subset_intervalOC

added theorem Set.bdd_below_bdd_above_iff_subset_interval

added theorem Set.dual_interval

added theorem Set.eq_of_mem_intervalOC_of_mem_intervalOC'

added theorem Set.eq_of_mem_intervalOC_of_mem_intervalOC

added theorem Set.eq_of_mem_interval_of_mem_interval'

added theorem Set.eq_of_mem_interval_of_mem_interval

added theorem Set.eq_of_not_mem_intervalOC_of_not_mem_intervalOC

added theorem Set.forall_intervalOC_iff

added def Set.interval

added def Set.intervalOC

added theorem Set.intervalOC_eq_union

added theorem Set.intervalOC_injective_left

added theorem Set.intervalOC_injective_right

added theorem Set.intervalOC_of_le

added theorem Set.intervalOC_of_lt

added theorem Set.intervalOC_subset_intervalOC_of_interval_subset_interval

added theorem Set.intervalOC_swap

added theorem Set.interval_eq_union

added theorem Set.interval_injective_left

added theorem Set.interval_injective_right

added theorem Set.interval_of_ge

added theorem Set.interval_of_gt

added theorem Set.interval_of_le

added theorem Set.interval_of_lt

added theorem Set.interval_of_not_ge

added theorem Set.interval_of_not_le

added theorem Set.interval_self

added theorem Set.interval_subset_Icc

added theorem Set.interval_subset_interval

added theorem Set.interval_subset_interval_iff_le'

added theorem Set.interval_subset_interval_iff_le

added theorem Set.interval_subset_interval_iff_mem

added theorem Set.interval_subset_interval_left

added theorem Set.interval_subset_interval_right

added theorem Set.interval_subset_interval_union_interval

added theorem Set.interval_swap

added theorem Set.left_mem_interval

added theorem Set.left_mem_intervalOC

added theorem Set.mem_interval

added theorem Set.mem_intervalOC

added theorem Set.mem_interval_of_ge

added theorem Set.mem_interval_of_le

added theorem Set.monotoneOn_or_antitoneOn_iff_interval

added theorem Set.monotone_or_antitone_iff_interval

added theorem Set.nonempty_interval

added theorem Set.not_mem_intervalOC

added theorem Set.not_mem_interval_of_gt

added theorem Set.not_mem_interval_of_lt

added theorem Set.right_mem_interval

added theorem Set.right_mem_intervalOC