cfcₙ_apply_mkD — Mathlib

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]

Похожие утверждения