Theorem BoundedContinuousFunction.exists_norm_eq_restrict_eq

Modification history

2026-07-20 01:34
Mathlib/Analysis/Complex/Tietze.lean
refactor: rename restrict to domRestrict (#25980) …
Deleted BoundedContinuousFunction.exists_norm_eq_restrict_eqView on Github →
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 →