gauge): gauge of a convex nhd of zero is continuous (#19102)

Commit

2 years ago

feat(analysis/convex/gauge): gauge of a convex nhd of zero is continuous (#19102) From the Brouwer Fixed Point Theorem project. Co-authored-by: @Shamrock-Frost

Author

urkud

Parents

e0736bb5

mathlib 373b03b5 - feat(analysis/convex/gauge): gauge of a convex nhd of zero is continuous (#19102)

mathlib
373b03b5 - feat(analysis/convex/gauge): gauge of a convex nhd of zero is continuous (#19102)