coe_bot — Mathlib

English

The underlying set of the bottom StarSubalgebra equals the range of the algebra map: ((⊥ : StarSubalgebra R A) : Set A) = Set.range (algebraMap R A).

Русский

Множество, лежащее в основе нижней StarSubalgebra, равно образу алгебраического отображения R → A.

LaTeX

$$$ ((\\bot : StarSubalgebra\\; R\\; A) : Set\\; A) = \\operatorname{range}(\\mathrm{algebraMap}\\; R\\; A) $$$

Lean4

@[simp, norm_cast]
theorem coe_bot : ((⊥ : StarSubalgebra R A) : Set A) = Set.range (algebraMap R A) :=
  rfl

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