Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-10 14:22 6bb17284

View on Github →

feat(analysis/convex): interiors/closures of convex sets are convex in a tvs (#1781)

  • feat(topology/algebra/module): scalar multiplication homeomorphisms
  • feat(topology/algebra/module): more lemmas
  • homeomorphisms given by scalar multiplication by unit is open/closed map.
  • feat(analysis/convex): interior of convex set is convex in a tvs
  • in separate file for interpretation time reasons.
  • feat(analysis/convex): extract lemma
  • feat(analysis/convex): closure of a convext set is convex
  • style(analysis/convex): place lemmas at reasonable locations
  • style(topology/algebra/module): fix bracketing style
  • feat(analysis/convex): introduce smul_set and pointwise_mul
  • also additional equivalent statements for convexity using those definitions.
  • feat(algebra/pointwise): lemmas for smul_set
  • doc(algebra/pointwise): add docstrings
  • doc(algebra/pointwise): add global docstring
  • docs(algebra/pointwise): amend global docstring

Estimated changes

added theorem set.one_smul_set
added def set.smul_set
added theorem zero_smul_set
added theorem convex_closure
added theorem convex_iff₂:
added theorem convex_iff₃:
added theorem convex_interior