setRange_algebraMap — Mathlib

English

The set range of the map algebraMap from S to A coincides with the underlying set of S inside A.

Русский

Множество значений отображения algebraMap из S в A совпадает с множеством элементов S внутри A.

LaTeX

$$$\Set.range(\mathrm{algebraMap}_{S}^{A}) = (S : \Set A)$$$

Lean4

@[simp]
theorem setRange_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
    Set.range (algebraMap S A) = (S : Set A) :=
  SetLike.ext'_iff.mp S.rangeS_algebraMap

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