mem_map — Mathlib

English

For any subring s ⊆ R and hom f: R →+* S, y ∈ s.map f iff ∃ x ∈ s with f x = y.

Русский

Для любого подполья s ⊆ R и гомоморфизма f: R →+* S, элемент y принадлежит образу s по f тогда и только тогда, когда существует x ∈ s с f(x) = y.

LaTeX

$$$y \\in s.map f \\iff \\exists x \\in s, f(x) = y.$$$

Lean4

@[simp]
theorem mem_map {f : R →+* S} {s : Subring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y :=
  Iff.rfl

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