Commit 2024-07-30 16:56 99914c54

View on Github →

chore(LocallyConvex/Bounded): rename variables (#15289) Instead of introducing a normed field 𝕜 and a nontrivially normed field 𝕝, prove a theorem for a normed field, then assume that 𝕜 is a nontrivially normed field.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

modified theorem Bornology.IsVonNBounded.smul_tendsto_zero

modified theorem Bornology.isVonNBounded_iff_smul_tendsto_zero

modified theorem Bornology.isVonNBounded_of_smul_tendsto_zero