Theorem exists_enorm_lt'

Modification history

2025-08-16 12:53
Mathlib/Analysis/Normed/Group/Basic.lean
feat: e-seminormed monoid (#27385) …
Modified exists_enorm_lt'View on Github →
2025-04-06 22:31
Mathlib/Analysis/Normed/Group/Basic.lean
feat(EGauge): add `egauge_pi` and `egauge_prod` (#23206) …
Added exists_enorm_lt'View on Github →