Theorem cfc_predicate_one

Modification history

2024-07-02 19:10
Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean
refactor: enforce the predicate on the `ContinuousFunctionalCalculus` is nontrivial (#14100) …
Added cfc_predicate_oneView on Github →