mem_fieldRange — Mathlib

English

For y in L', y belongs to the fieldRange of f if and only if there exists x in L with f(x) = y.

Русский

Для элемента y ∈ L' верно: y принадлежит образу поля f тогда и только тогда, когда существует x ∈ L такое, что f(x) = y.

LaTeX

$$$ y \\in f.fieldRange \\iff \\exists x \\in L, f(x) = y $$$

Lean4

@[simp]
theorem mem_fieldRange {y : L'} : y ∈ f.fieldRange ↔ ∃ x, f x = y :=
  Iff.rfl

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