preimage — Mathlib

English

The preimage of a set s by f is the set of x with f(x) ∈ s.

Русский

Образ предобраза множества s по отображению f — это множество x such that f(x) ∈ s.

LaTeX

$$$\\mathrm{preimage}(f,s) = \\{ x \\mid f(x) \\in s \\}$$$

Lean4

/-- The preimage of `s : Set β` by `f : α → β`, written `f ⁻¹' s`,
  is the set of `x : α` such that `f x ∈ s`. -/
def preimage (f : α → β) (s : Set β) : Set α :=
  {x | f x ∈ s}

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