cfcₙ_zero — Mathlib

English

If two functions agree on the spectrum, then their calculus outputs are equal.

Русский

Если две функции согласуются на спектре, то их результаты калькулятора равны.

LaTeX

$$Set.EqOn f g (quasispectrum R a) → cfcₙ f a = cfcₙ g a$$

Lean4

@[simp]
theorem cfcₙ_zero : cfcₙ (0 : R → R) a = 0 := by
  by_cases ha : p a
  · exact cfcₙ_apply (0 : R → R) a ▸ map_zero (cfcₙHom ha)
  · rw [cfcₙ_apply_of_not_predicate a ha]

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