Theorem infEDist_smul_of_nonempty₀

Modification history

2026-10-28 01:55
Mathlib/Analysis/Normed/Module/Ball/Pointwise.lean
refactor(Analysis/Normed): generalize scalar distance and diameter lemmas (#44829) …
Added infEDist_smul_of_nonempty₀View on Github →