continuous_selfAdjointPart — Mathlib

English

The self-adjoint part map is a continuous function from A to A, where self-adjoint part is defined with respect to the star-involution.

Русский

Отображение на самосопряженную часть является непрерывной функцией из A в A (часть определяется через звезду).

LaTeX

$$$\text{continuous_selfAdjointPart}: A \to C \subseteq A \text{ is continuous}$$$

Lean4

theorem continuous_selfAdjointPart [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] :
    Continuous (selfAdjointPart R (A := A)) :=
  ((continuous_const_smul _).comp <| continuous_id.add continuous_star).subtype_mk _

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