realPart_surjective — Mathlib

English

The real part map is surjective onto the self-adjoint elements; every self-adjoint element is the real part of some element.

Русский

Действительная часть сюръективна на selfAdjoint; каждый selfAdjoint элемент является действительной частью некоторого элемента.

LaTeX

$$$\\text{surjective}(\\operatorname{realPart})$ onto $\\operatorname{selfAdjoint}(A)$$$

Lean4

theorem realPart_surjective : Function.Surjective (realPart (A := A)) := fun x ↦
  ⟨(x : A), Subtype.ext x.property.coe_realPart⟩

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