Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-02 12:18 1843bfc9

View on Github →

feat(algebra/pointwise): pointwise scalar-multiplication lemmas (#1925)

  • feat(algebra/pointwise): more lemmas about scaling sets
  • rename smul_set to scale_set for disambiguation
  • define scale_set_action, which subsumes one_smul_set
  • additional lemmas lemmas
  • fix(analysis/convex): refactor proofs for scale_set
  • feat(algebra/pointwise): re-organise file
  • subsume pointwise_mul_action
  • feat(algebra/pointwise): remove pointwise_mul_action
  • subsumed by smul_set_action with left-regular action.

Estimated changes

added theorem mem_inv_smul_set_iff
modified theorem set.mem_smul_set
deleted theorem set.one_smul_set
added theorem set.smul_mem_smul_set
added theorem set.smul_set_empty
modified theorem set.smul_set_eq_image
added theorem set.smul_set_mono
added theorem set.smul_set_union