Theorem Bornology.IsBounded.exists_pos_norm_le'

Modification history

2024-06-18 08:57

Mathlib/Analysis/Normed/Group/Basic.lean

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

Modified Bornology.IsBounded.exists_pos_norm_le'View on Github →

2023-09-19 04:03

Mathlib/Analysis/Normed/Group/Basic.lean

refactor(Topology/MetricSpace): remove `Metric.Bounded` (#7240) …

Added Bornology.IsBounded.exists_pos_norm_le'View on Github →