cfc_apply_of_not_and — Mathlib

English

If it is not the case that p(a) holds together with f being continuous on the spectrum of a, then cfc f a vanishes: cfc f a = 0.

Русский

Если не выполняется условие p(a) и непрерывность f на спектре a, то cfc f a = 0.

LaTeX

$$$ \neg\big(p(a) \wedge \text{ContinuousOn}(f, \text{ spectrum } R a)\big) \Rightarrow cfc\, f\, a = 0 $$$

Lean4

theorem cfc_apply_of_not_and {f : R → R} (a : A) (ha : ¬(p a ∧ ContinuousOn f (spectrum R a))) : cfc f a = 0 := by
  rw [cfc_def, dif_neg ha]

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