mem_map — Mathlib

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

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