cfc_congr — Mathlib

English

If f and g agree on the spectrum of a, then cfc f a equals cfc g a.

Русский

Если f и g совпадают на спектре a, то cfc f a = cfc g a.

LaTeX

$$spectrum R a .EqOn f g \Rightarrow cfc f a = cfc g a$$

Lean4

theorem cfc_congr {f g : R → R} {a : A} (hfg : (spectrum R a).EqOn f g) : cfc f a = cfc g a :=
  by
  by_cases h : p a ∧ ContinuousOn g (spectrum R a)
  · rw [cfc_apply (ha := h.1) (hf := h.2.congr hfg), cfc_apply (ha := h.1) (hf := h.2)]
    congr 2
    exact Set.restrict_eq_iff.mpr hfg
  · obtain (ha | hg) := not_and_or.mp h
    · simp [cfc_apply_of_not_predicate a ha]
    · rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn]
      exact fun hf ↦ hg (hf.congr hfg.symm)

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