English
Given a property P on A and a, the statement cfc_cases says: either p(a) ∧ ContinuousOn f on spectrum or one of the negations holds, and in each branch P(cfc f a) follows.
Русский
Для любой свойства P на A и элемента a выражение cfc_cases говорит: либо p(a) ∧ ContinuousOn f на спектре, либо одно из отрицаний выполняется; в каждой ветви следует P(cfc f a).
LaTeX
$$$ \text{cfc_cases}(P,a,f,h_0,haf) : P(cfc f a) $ (формулировка, охватывающая случаи).$$
Lean4
theorem cfc_cases (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0)
(haf : (hf : ContinuousOn f (spectrum R a)) → (ha : p a) → P (cfcHom ha ⟨_, hf.restrict⟩)) : P (cfc f a) :=
by
by_cases h : p a ∧ ContinuousOn f (spectrum R a)
· rw [cfc_apply f a h.1 h.2]
exact haf h.2 h.1
· simp only [not_and_or] at h
obtain (h | h) := h
· rwa [cfc_apply_of_not_predicate _ h]
· rwa [cfc_apply_of_not_continuousOn _ h]
