toNonUnital — Mathlib

English

If ha holds and f ≤ g in the function ordering, then cfc_nHom ha f ≤ cfc_nHom ha g.

Русский

Если ha выполняется и f ≤ g по порядку функций, тогда cfc_nHom ha f ≤ cfc_nHom ha g.

LaTeX

$$$$ cfc\\!_nHom ha f \\le cfc\\!_nHom ha g $$$$

Lean4

instance toNonUnital : NonUnitalContinuousFunctionalCalculus R A p
    where
  predicate_zero := cfc_predicate_zero R
  compactSpace_quasispectrum
    a := by
    have h_cpct : CompactSpace (spectrum R a) := inferInstance
    simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢
    exact h_cpct |>.union isCompact_singleton
  exists_cfc_of_predicate _
    ha :=
    ⟨cfcₙHom_of_cfcHom R ha, isClosedEmbedding_cfcₙHom_of_cfcHom ha, cfcHom_id ha,
      cfcₙHom_of_cfcHom_map_quasispectrum ha, fun _ ↦ cfcHom_predicate ha _⟩

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