Theorem BoundedContinuousFunction.exists_norm_eq_restrict_eq

Modification history

2024-02-15 16:15
Mathlib/Analysis/Complex/Tietze.lean
feat: add a `TietzeExtension` class (#9788) …
Added BoundedContinuousFunction.exists_norm_eq_restrict_eqView on Github →