Theorem interior_sphere

Modification history

2024-02-06 07:03

Mathlib/Analysis/NormedSpace/Basic.lean

chore(NormedSpace/Basic): move some theorems to `NormedSpace.Real` (#10206) …

Modified interior_sphere View on Github →

2023-04-28 06:56

Mathlib/Analysis/NormedSpace/Basic.lean

chore: forward-port leanprover-community/mathlib#18869 (#3676)

Added interior_sphere View on Github →