Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-12 17:56 9003f287

View on Github →

chore(data/set/intervals/unordered_interval): Rename to uIcc/uIoc (#18104) Rename

set.interval → set.uIcc
set.interval_oc → set.uIoc
finset.interval→ finset.uIcc Closes #17982 Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Set.20intervals.20names

Estimated changes

Modified src/analysis/ODE/picard_lindelof.lean

Modified src/analysis/calculus/parametric_interval_integral.lean

Modified src/analysis/complex/cauchy_integral.lean

Modified src/analysis/convex/basic.lean

deleted theorem convex_interval

added theorem convex_uIcc

Modified src/analysis/convex/quasiconvex.lean

deleted theorem quasilinear_on_iff_mem_interval

added theorem quasilinear_on_iff_mem_uIcc

Modified src/analysis/convex/segment.lean

deleted theorem segment_eq_interval

added theorem segment_eq_uIcc

deleted theorem segment_subset_interval

added theorem segment_subset_uIcc

Modified src/analysis/convex/star.lean

Modified src/analysis/convex/strict.lean

deleted theorem strict_convex_interval

deleted theorem strict_convex_interval_oc

added theorem strict_convex_uIcc

added theorem strict_convex_uIoc

Modified src/analysis/special_functions/integrals.lean

deleted theorem integral_pow_abs_sub_interval_oc

added theorem integral_pow_abs_sub_uIoc

Modified src/analysis/special_functions/non_integrable.lean

Modified src/analysis/sum_integral_comparisons.lean

Modified src/data/finset/locally_finite.lean

deleted theorem finset.Icc_subset_interval'

deleted theorem finset.Icc_subset_interval

added theorem finset.Icc_subset_uIcc'

added theorem finset.Icc_subset_uIcc

deleted theorem finset.eq_of_mem_interval_of_mem_interval'

deleted theorem finset.eq_of_mem_interval_of_mem_interval

added theorem finset.eq_of_mem_uIcc_of_mem_uIcc'

added theorem finset.eq_of_mem_uIcc_of_mem_uIcc

deleted theorem finset.interval_eq_union

deleted theorem finset.interval_injective_left

deleted theorem finset.interval_injective_right

deleted theorem finset.interval_of_ge

deleted theorem finset.interval_of_le

deleted theorem finset.interval_of_not_ge

deleted theorem finset.interval_of_not_le

deleted theorem finset.interval_self

deleted theorem finset.interval_subset_Icc

deleted theorem finset.interval_subset_interval

deleted theorem finset.interval_subset_interval_iff_le'

deleted theorem finset.interval_subset_interval_iff_le

deleted theorem finset.interval_subset_interval_iff_mem

deleted theorem finset.interval_subset_interval_left

deleted theorem finset.interval_subset_interval_right

deleted theorem finset.interval_subset_interval_union_interval

deleted theorem finset.interval_swap

deleted theorem finset.interval_to_dual

deleted theorem finset.left_mem_interval

added theorem finset.left_mem_uIcc

deleted theorem finset.mem_interval'

deleted theorem finset.mem_interval_of_ge

deleted theorem finset.mem_interval_of_le

added theorem finset.mem_uIcc'

added theorem finset.mem_uIcc_of_ge

added theorem finset.mem_uIcc_of_le

deleted theorem finset.nonempty_interval

added theorem finset.nonempty_uIcc

deleted theorem finset.not_mem_interval_of_gt

deleted theorem finset.not_mem_interval_of_lt

added theorem finset.not_mem_uIcc_of_gt

added theorem finset.not_mem_uIcc_of_lt

deleted theorem finset.right_mem_interval

added theorem finset.right_mem_uIcc

added theorem finset.uIcc_comm

added theorem finset.uIcc_eq_union

added theorem finset.uIcc_injective_left

added theorem finset.uIcc_injective_right

added theorem finset.uIcc_of_ge

added theorem finset.uIcc_of_le

added theorem finset.uIcc_of_not_ge

added theorem finset.uIcc_of_not_le

added theorem finset.uIcc_self

added theorem finset.uIcc_subset_Icc

added theorem finset.uIcc_subset_uIcc

added theorem finset.uIcc_subset_uIcc_iff_le'

added theorem finset.uIcc_subset_uIcc_iff_le

added theorem finset.uIcc_subset_uIcc_iff_mem

added theorem finset.uIcc_subset_uIcc_left

added theorem finset.uIcc_subset_uIcc_right

added theorem finset.uIcc_subset_uIcc_union_uIcc

added theorem finset.uIcc_to_dual

Modified src/data/set/intervals/ord_connected.lean

deleted theorem set.ord_connected.interval_oc_subset

deleted theorem set.ord_connected.interval_subset

added theorem set.ord_connected.uIcc_subset

added theorem set.ord_connected.uIoc_subset

deleted theorem set.ord_connected_iff_interval_subset

deleted theorem set.ord_connected_iff_interval_subset_left

deleted theorem set.ord_connected_iff_interval_subset_right

added theorem set.ord_connected_iff_uIcc_subset

added theorem set.ord_connected_iff_uIcc_subset_left

added theorem set.ord_connected_iff_uIcc_subset_right

deleted theorem set.ord_connected_interval

deleted theorem set.ord_connected_interval_oc

deleted theorem set.ord_connected_of_interval_subset_left

added theorem set.ord_connected_of_uIcc_subset_left

added theorem set.ord_connected_uIcc

added theorem set.ord_connected_uIoc

Modified src/data/set/intervals/ord_connected_component.lean

deleted theorem set.eq_of_mem_ord_connected_section_of_interval_subset

added theorem set.eq_of_mem_ord_connected_section_of_uIcc_subset

modified theorem set.ord_connected_component_subset

Modified src/data/set/intervals/unordered_interval.lean

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_interval_oc'

deleted theorem set.Ioc_subset_interval_oc

added theorem set.Ioc_subset_uIoc'

added theorem set.Ioc_subset_uIoc

deleted theorem set.bdd_below_bdd_above_iff_subset_interval

added theorem set.bdd_below_bdd_above_iff_subset_uIcc

deleted theorem set.dual_interval

added theorem set.dual_uIcc

deleted theorem set.eq_of_mem_interval_oc_of_mem_interval_oc'

deleted theorem set.eq_of_mem_interval_oc_of_mem_interval_oc

deleted theorem set.eq_of_mem_interval_of_mem_interval'

deleted theorem set.eq_of_mem_interval_of_mem_interval

added theorem set.eq_of_mem_uIcc_of_mem_uIcc'

added theorem set.eq_of_mem_uIcc_of_mem_uIcc

added theorem set.eq_of_mem_uIoc_of_mem_uIoc'

added theorem set.eq_of_mem_uIoc_of_mem_uIoc

deleted theorem set.eq_of_not_mem_interval_oc_of_not_mem_interval_oc

added theorem set.eq_of_not_mem_uIoc_of_not_mem_uIoc

deleted theorem set.forall_interval_oc_iff

added theorem set.forall_uIoc_iff

deleted def set.interval

deleted theorem set.interval_eq_union

deleted theorem set.interval_injective_left

deleted theorem set.interval_injective_right

deleted def set.interval_oc

deleted theorem set.interval_oc_eq_union

deleted theorem set.interval_oc_injective_left

deleted theorem set.interval_oc_injective_right

deleted theorem set.interval_oc_of_le

deleted theorem set.interval_oc_of_lt

deleted theorem set.interval_oc_subset_interval_oc_of_interval_subset_interval

deleted theorem set.interval_oc_swap

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_subset_interval

deleted theorem set.interval_subset_interval_iff_le'

deleted theorem set.interval_subset_interval_iff_le

deleted theorem set.interval_subset_interval_iff_mem

deleted theorem set.interval_subset_interval_left

deleted theorem set.interval_subset_interval_right

deleted theorem set.interval_subset_interval_union_interval

deleted theorem set.interval_swap

deleted theorem set.left_mem_interval

deleted theorem set.left_mem_interval_oc

added theorem set.left_mem_uIcc

added theorem set.left_mem_uIoc

deleted theorem set.mem_interval

deleted theorem set.mem_interval_oc

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.monotone_on_or_antitone_on_iff_interval

added theorem set.monotone_on_or_antitone_on_iff_uIcc

deleted theorem set.monotone_or_antitone_iff_interval

added theorem set.monotone_or_antitone_iff_uIcc

deleted theorem set.nonempty_interval

added theorem set.nonempty_uIcc

deleted theorem set.not_mem_interval_oc

deleted theorem set.not_mem_interval_of_gt

deleted theorem set.not_mem_interval_of_lt

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_interval_oc

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_injective_left

added theorem set.uIcc_injective_right

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 theorem set.uIcc_subset_uIcc_iff_le'

added theorem set.uIcc_subset_uIcc_iff_le

added theorem set.uIcc_subset_uIcc_iff_mem

added theorem set.uIcc_subset_uIcc_left

added theorem set.uIcc_subset_uIcc_right

added theorem set.uIcc_subset_uIcc_union_uIcc

added def set.uIoc

added theorem set.uIoc_eq_union

added theorem set.uIoc_injective_left

added theorem set.uIoc_injective_right

added theorem set.uIoc_of_le

added theorem set.uIoc_of_lt

added theorem set.uIoc_subset_uIoc_of_uIcc_subset_uIcc

added theorem set.uIoc_swap

Modified src/data/set/pointwise/interval.lean

deleted theorem set.abs_sub_le_of_subinterval

added theorem set.abs_sub_le_of_uIcc_subset_uIcc

deleted theorem set.abs_sub_left_of_mem_interval

added theorem set.abs_sub_left_of_mem_uIcc

deleted theorem set.abs_sub_right_of_mem_interval

added theorem set.abs_sub_right_of_mem_uIcc

deleted theorem set.image_add_const_interval

added theorem set.image_add_const_uIcc

deleted theorem set.image_const_add_interval

added theorem set.image_const_add_uIcc

deleted theorem set.image_const_mul_interval

added theorem set.image_const_mul_uIcc

deleted theorem set.image_const_sub_interval

added theorem set.image_const_sub_uIcc

deleted theorem set.image_div_const_interval

added theorem set.image_div_const_uIcc

deleted theorem set.image_mul_const_interval

added theorem set.image_mul_const_uIcc

deleted theorem set.image_neg_interval

added theorem set.image_neg_uIcc

deleted theorem set.image_sub_const_interval

added theorem set.image_sub_const_uIcc

deleted theorem set.preimage_add_const_interval

added theorem set.preimage_add_const_uIcc

deleted theorem set.preimage_const_add_interval

added theorem set.preimage_const_add_uIcc

deleted theorem set.preimage_const_mul_interval

added theorem set.preimage_const_mul_uIcc

deleted theorem set.preimage_const_sub_interval

added theorem set.preimage_const_sub_uIcc

deleted theorem set.preimage_div_const_interval

added theorem set.preimage_div_const_uIcc

deleted theorem set.preimage_mul_const_interval

added theorem set.preimage_mul_const_uIcc

deleted theorem set.preimage_neg_interval

added theorem set.preimage_neg_uIcc

deleted theorem set.preimage_sub_const_interval

added theorem set.preimage_sub_const_uIcc

Modified src/linear_algebra/affine_space/affine_map.lean

deleted theorem affine_map.image_interval

added theorem affine_map.image_uIcc

Modified src/measure_theory/constructions/borel_space.lean

deleted theorem measurable_set_interval

deleted theorem measurable_set_interval_oc

added theorem measurable_set_uIcc

added theorem measurable_set_uIoc

Modified src/measure_theory/function/locally_integrable.lean

deleted theorem continuous.integrable_on_interval

deleted theorem continuous.integrable_on_interval_oc

added theorem continuous.integrable_on_uIcc

added theorem continuous.integrable_on_uIoc

deleted theorem continuous_on.integrable_on_interval

added theorem continuous_on.integrable_on_uIcc

Modified src/measure_theory/function/strongly_measurable/basic.lean

deleted theorem measure_theory.ae_strongly_measurable.ae_strongly_measurable_interval_oc_iff

added theorem measure_theory.ae_strongly_measurable.ae_strongly_measurable_uIoc_iff

Modified src/measure_theory/integral/circle_integral.lean

Modified src/measure_theory/integral/circle_transform.lean

Modified src/measure_theory/integral/divergence_theorem.lean

Modified src/measure_theory/integral/integral_eq_improper.lean

Modified src/measure_theory/integral/interval_average.lean

Modified src/measure_theory/integral/interval_integral.lean

modified theorem antitone_on.interval_integrable

deleted theorem interval_integral.abs_integral_eq_abs_integral_interval_oc

added theorem interval_integral.abs_integral_eq_abs_integral_uIoc

modified theorem interval_integral.integral_deriv_eq_sub

modified theorem interval_integral.integral_eq_sub_of_has_deriv_right

modified theorem interval_integral.interval_integrable_deriv_of_nonneg

deleted theorem interval_integral.interval_integral_eq_integral_interval_oc

added theorem interval_integral.interval_integral_eq_integral_uIoc

modified theorem monotone_on.interval_integrable

Modified src/measure_theory/integral/layercake.lean

Modified src/measure_theory/measure/ae_measurable.lean

deleted theorem ae_measurable_interval_oc_iff

added theorem ae_measurable_uIoc_iff

Modified src/measure_theory/measure/lebesgue.lean

modified theorem real.volume_interval

Modified src/measure_theory/measure/measure_space.lean

deleted theorem measure_theory.ae_interval_oc_iff

deleted theorem measure_theory.ae_restrict_interval_oc_eq

deleted theorem measure_theory.ae_restrict_interval_oc_iff

added theorem measure_theory.ae_restrict_uIoc_eq

added theorem measure_theory.ae_restrict_uIoc_iff

added theorem measure_theory.ae_uIoc_iff

deleted theorem measure_theory.interval_oc_ae_eq_interval

added theorem measure_theory.uIoc_ae_eq_interval

Modified src/order/filter/interval.lean

deleted theorem filter.tendsto.interval

added theorem filter.tendsto.uIcc

Modified src/order/locally_finite.lean

deleted theorem finset.coe_interval

added theorem finset.coe_uIcc

deleted def finset.interval

deleted theorem finset.mem_interval

added theorem finset.mem_uIcc

added def finset.uIcc

deleted theorem prod.card_interval

added theorem prod.card_uIcc

deleted theorem prod.interval_eq

deleted theorem prod.interval_mk_mk

added theorem prod.uIcc_eq

added theorem prod.uIcc_mk_mk

Modified src/topology/algebra/order/compact.lean

deleted theorem continuous_on.image_interval

deleted theorem continuous_on.image_interval_eq_Icc

added theorem continuous_on.image_uIcc

added theorem continuous_on.image_uIcc_eq_Icc

deleted theorem is_compact_interval

added theorem is_compact_uIcc

Modified src/topology/algebra/order/intermediate_value.lean

deleted theorem continuous_on.surj_on_interval

added theorem continuous_on.surj_on_uIcc

deleted theorem intermediate_value_interval

added theorem intermediate_value_uIcc

deleted theorem is_preconnected_interval

added theorem is_preconnected_uIcc

Modified src/topology/algebra/order/t5.lean

Modified src/topology/metric_space/basic.lean

deleted theorem real.dist_le_of_mem_interval

added theorem real.dist_le_of_mem_uIcc

deleted theorem real.dist_left_le_of_mem_interval

added theorem real.dist_left_le_of_mem_uIcc

deleted theorem real.dist_right_le_of_mem_interval

added theorem real.dist_right_le_of_mem_uIcc