English
Let S be a StarSubalgebra of A and f: A →⋆ₐ[R] B. For y ∈ B, y lies in the image map f of S if and only if there exists x ∈ S with f(x) = y.
Русский
Пусть S — звездная подсалгебра A и f: A →⋆ₐ[R] B. Тогда y ∈ map f S тогда и только тогда, когда существует x ∈ S такое, что f(x) = y.
LaTeX
$$$y \\in \\mathrm{map}\;f\\;S \\iff \\exists x \\in S: f(x) = y$$$
Lean4
@[simp]
theorem mem_map {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {y : B} : y ∈ map f S ↔ ∃ x ∈ S, f x = y :=
Subsemiring.mem_map