cfcₙ_cases — Mathlib

English

If f is not continuous on the spectrum, then cfcₙ f a = 0.

Русский

Если f не непрерывна на спектре, то cfcₙ f a = 0.

LaTeX

$$Not (ContinuousOn f (quasispectrum R a)) → cfcₙ f a = 0$$

Lean4

theorem cfcₙ_cases (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0)
    (haf : ∀ (hf : ContinuousOn f (σₙ R a)) h0 ha, P (cfcₙHom ha ⟨⟨_, hf.restrict⟩, h0⟩)) : P (cfcₙ f a) :=
  by
  by_cases h : ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a
  · rw [cfcₙ_apply f a h.1 h.2.1 h.2.2]
    exact haf h.1 h.2.1 h.2.2
  · simp only [not_and_or] at h
    obtain (h | h | h) := h
    · rwa [cfcₙ_apply_of_not_continuousOn _ h]
    · rwa [cfcₙ_apply_of_not_map_zero _ h]
    · rwa [cfcₙ_apply_of_not_predicate _ h]

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