Commit 2023-04-19 11:19 a12b7114

View on Github →

feat: port Analysis.NormedSpace.BallAction (#3513)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/BallAction.lean

added theorem ne_neg_of_mem_sphere

added theorem ne_neg_of_mem_unit_sphere