Commit 2023-01-22 15:33 bd0eb8a4

View on Github →

chore: Rename intervals to uIcc/uIoc (#1496) Match https://github.com/leanprover-community/mathlib/pull/18104

Estimated changes

deleted theorem Set.ordConnected_interval
added theorem Set.ordConnected_uIcc
added theorem Set.ordConnected_uIoc
deleted theorem Set.Icc_subset_interval'
deleted theorem Set.Icc_subset_interval
added theorem Set.Icc_subset_uIcc'
added theorem Set.Icc_subset_uIcc
deleted theorem Set.Ioc_subset_intervalOC
added theorem Set.Ioc_subset_uIoc'
added theorem Set.Ioc_subset_uIoc
deleted theorem Set.dual_interval
added theorem Set.dual_uIcc
deleted theorem Set.forall_intervalOC_iff
added theorem Set.forall_uIoc_iff
deleted def Set.interval
deleted def Set.intervalOC
deleted theorem Set.intervalOC_eq_union
deleted theorem Set.intervalOC_of_le
deleted theorem Set.intervalOC_of_lt
deleted theorem Set.intervalOC_swap
deleted theorem Set.interval_eq_union
deleted theorem Set.interval_of_ge
deleted theorem Set.interval_of_gt
deleted theorem Set.interval_of_le
deleted theorem Set.interval_of_lt
deleted theorem Set.interval_of_not_ge
deleted theorem Set.interval_of_not_le
deleted theorem Set.interval_self
deleted theorem Set.interval_subset_Icc
deleted theorem Set.interval_swap
deleted theorem Set.left_mem_interval
deleted theorem Set.left_mem_intervalOC
added theorem Set.left_mem_uIcc
added theorem Set.left_mem_uIoc
deleted theorem Set.mem_interval
deleted theorem Set.mem_intervalOC
deleted theorem Set.mem_interval_of_ge
deleted theorem Set.mem_interval_of_le
added theorem Set.mem_uIcc
added theorem Set.mem_uIcc_of_ge
added theorem Set.mem_uIcc_of_le
added theorem Set.mem_uIoc
deleted theorem Set.nonempty_interval
added theorem Set.nonempty_uIcc
deleted theorem Set.not_mem_intervalOC
added theorem Set.not_mem_uIcc_of_gt
added theorem Set.not_mem_uIcc_of_lt
added theorem Set.not_mem_uIoc
deleted theorem Set.right_mem_interval
deleted theorem Set.right_mem_intervalOC
added theorem Set.right_mem_uIcc
added theorem Set.right_mem_uIoc
added def Set.uIcc
added theorem Set.uIcc_comm
added theorem Set.uIcc_eq_union
added theorem Set.uIcc_of_ge
added theorem Set.uIcc_of_gt
added theorem Set.uIcc_of_le
added theorem Set.uIcc_of_lt
added theorem Set.uIcc_of_not_ge
added theorem Set.uIcc_of_not_le
added theorem Set.uIcc_self
added theorem Set.uIcc_subset_Icc
added theorem Set.uIcc_subset_uIcc
added def Set.uIoc
added theorem Set.uIoc_comm
added theorem Set.uIoc_eq_union
added theorem Set.uIoc_of_le
added theorem Set.uIoc_of_lt