Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bounded_continuous_function.star_apply

Modification history

2021-12-09 19:38
src/topology/continuous_function/bounded.lean
feat(topology/continuous_function/bounded): register instances of `star` structures (#10570) …
Added bounded_continuous_function.star_applyView on Github →