Theorem IsCompact.exists_bound_of_continuous_on'

Modification history

2023-09-04 12:27
Mathlib/Analysis/Normed/Group/Basic.lean
chore(Analysis): rename lipschitz_on_univ to lipschitzOn_univ (#6946) …
Deleted IsCompact.exists_bound_of_continuous_on'View on Github →
2023-03-09 06:58
Mathlib/Analysis/Normed/Group/Basic.lean
feat: port Analysis.Normed.Group.Basic (#2736)
Added IsCompact.exists_bound_of_continuous_on'View on Github →