mem_range — Mathlib

English

The range of φ contains exactly those elements y for which y = φ(x) for some x in A.

Русский

Образ φ содержит ровно те элементы y, которые равны φ(x) для некоторого x в A.

LaTeX

$$y ∈ NonUnitalStarAlgHom.range φ ⇔ ∃ x : A, φ x = y$$

Lean4

@[simp]
theorem mem_range (φ : F) {y : B} :
    y ∈ (NonUnitalStarAlgHom.range φ : NonUnitalStarSubalgebra R B) ↔ ∃ x : A, φ x = y :=
  NonUnitalRingHom.mem_srange

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