cfc_eq_cfc_iff_eqOn — Mathlib

English

Equality of cfc values is equivalent to equality on the spectrum: cfc f a = cfc g a iff (spectrum R a).EqOn f g, under appropriate predicates and continuity assumptions.

Русский

Равенство значений cfc эквивалентно равенству на спектре: cfc f a = cfc g a тогда и только тогда, когда (spectrum R a).EqOn f g, при соответствующих условиях.

LaTeX

$$$ cfc f a = cfc g a \iff (spectrum R a).EqOn f g $$$

Lean4

theorem cfc_eq_cfc_iff_eqOn : cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
  ⟨eqOn_of_cfc_eq_cfc, cfc_congr⟩

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