Theorem IsCompact.exists_bound_of_continuousOn'

Modification history

2024-06-18 08:57

Mathlib/Analysis/Normed/Group/Basic.lean

chore(Analysis/Normed/Group): Move boundedness lemmas (#13895) …

Modified IsCompact.exists_bound_of_continuousOn'View on Github →

2023-09-04 12:27

Mathlib/Analysis/Normed/Group/Basic.lean

chore(Analysis): rename lipschitz_on_univ to lipschitzOn_univ (#6946) …

Added IsCompact.exists_bound_of_continuousOn'View on Github →