Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-04 22:11 253f75c8

View on Github →

feat(data/set/intervals): define intervals and prove basic properties (#1949)

  • things about intervals
  • better documentation
  • better file name
  • add segment_eq_interval
  • better proof for is_measurable_interval
  • better import and better proof
  • better proof

Estimated changes

added theorem max_sub_min_eq_abs'
added theorem max_sub_min_eq_abs
added theorem segment_eq_interval
added theorem set.indicator_apply
added theorem set.indicator_mul
added theorem set.indicator_nonneg'
added theorem set.indicator_nonneg
added theorem set.indicator_nonpos'
added theorem set.indicator_nonpos
added def set.interval
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_swap
added theorem set.left_mem_interval
added theorem set.mem_interval_of_ge
added theorem set.mem_interval_of_le
added theorem set.nonempty_interval
added theorem set.right_mem_interval
added theorem is_measurable_interval
added theorem real.volume_Icc
added theorem real.volume_Ico
added theorem real.volume_Ioo
added theorem real.volume_interval
added theorem real.volume_singleton
added theorem real.volume_val