Commit 2024-06-05 15:42 604b60d9

View on Github →

chore(LocallyConvex/Bounded): use implicit args (#13531) Also generalize some lemmas, most importantly isVonNBounded_of_isBounded, from NontriviallyNormedField to NormedField.

Estimated changes

Modified Mathlib/Analysis/Convex/GaugeRescale.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

modified theorem NormedSpace.image_isVonNBounded_iff

modified theorem NormedSpace.isVonNBounded_ball

modified theorem NormedSpace.isVonNBounded_iff'

modified theorem NormedSpace.isVonNBounded_iff

added theorem NormedSpace.isVonNBounded_of_isBounded

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean