map_star — Mathlib

English

The spectrum map respects star: map_star(a) shows that the spectrum of star a is the star of the spectrum of a.

Русский

Карта спектра сохраняет операцию звезды: спектр от star a равен звезде спектра a.

LaTeX

$$$\operatorname{map\_star}(a) : \sigma(\star a) = \star (\sigma a)$$$

Lean4

protected theorem map_star (a : A) : σ (star a) = star (σ a) :=
  by
  ext
  simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm

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