English
Theorem that handles all cases of applicability of cfc by splitting on continuity, map-zero, and predicate.
Русский
Теорема, распределяющая случаи применения cfc по непрерывности, нулю и предикату.
LaTeX
$$cfcₙ_cases ...$$
Lean4
theorem cfcₙ_congr {f g : R → R} {a : A} (hfg : (σₙ R a).EqOn f g) : cfcₙ f a = cfcₙ g a :=
by
by_cases h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
· rw [cfcₙ_apply f a (h.2.1.congr hfg) (hfg (quasispectrum.zero_mem R a) ▸ h.2.2) h.1, cfcₙ_apply g a h.2.1 h.2.2 h.1]
congr 3
exact Set.restrict_eq_iff.mpr hfg
· simp only [not_and_or] at h
obtain (ha | hg | h0) := 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)
· rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero]
exact fun hf ↦ h0 (hfg (quasispectrum.zero_mem R a) ▸ hf)
