Theorem BoundedContinuousFunction.exists_forall_mem_domRestrict_eq_of_closed

Modification history

2026-07-20 01:34
Mathlib/Topology/TietzeExtension.lean
refactor: rename restrict to domRestrict (#25980) …
Added BoundedContinuousFunction.exists_forall_mem_domRestrict_eq_of_closedView on Github →