Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-08 15:10 65a5dc0f

View on Github →

feat(data/support): define support of a function and prove some properties (#2340)

  • feat(data/support): define support of a function and prove some properties
  • Add support_mul' for group_with_zero

Estimated changes

added theorem set.support_indicator
added theorem function.nmem_support
added def function.support
added theorem function.support_add
added theorem function.support_comp'
added theorem function.support_comp
added theorem function.support_div
added theorem function.support_inf
added theorem function.support_infi
added theorem function.support_inv
added theorem function.support_max
added theorem function.support_min
added theorem function.support_mul'
added theorem function.support_mul
added theorem function.support_neg
added theorem function.support_prod
added theorem function.support_sub
added theorem function.support_sum
added theorem function.support_sup
added theorem function.support_supr