Commit 2024-03-10 18:54 533116b3

View on Github →

feat(ConstMulAction): add closure_smul₀', generalize (#10860)

  • Add closure_smul₀', a version of closure_smul₀ assuming c ≠ 0 and no T1Space.
  • Generalize some lemmas from TVS to a continuous MulActionWithZero.

Estimated changes

modified theorem IsClosed.smul₀
added theorem closure_smul₀'
modified theorem isClosedMap_smul₀