English
If two functions agree on the spectrum then they produce equal outputs under cfc.
Русский
Если две функции совпадают на спектре, то они дают равные значения под cfc.
LaTeX
$$Set.EqOn f g (quasispectrum R a) → cfcₙ f a = cfcₙ g a$$
Lean4
/-- A version of `cfcₙ_apply` in terms of `ContinuousMapZero.mkD` -/
theorem cfcₙ_apply_mkD : cfcₙ f a = cfcₙHom (a := a) ha (mkD ((quasispectrum R a).restrict f) 0) :=
by
by_cases f_cont : ContinuousOn f (quasispectrum R a)
· by_cases f_zero : f 0 = 0
· rw [cfcₙ_apply f a, mkD_of_continuousOn f_cont f_zero]
· rw [cfcₙ_apply_of_not_map_zero a f_zero, mkD_of_not_zero, map_zero]
exact f_zero
· rw [cfcₙ_apply_of_not_continuousOn a f_cont, mkD_of_not_continuousOn f_cont, map_zero]