image_def

Mathlib.Data.PFun

URI: https://scilib.ai/kg/mathlib#PFun.image_def

English

For any f, the image of s is the set of y for which there exists x ∈ s with y ∈ f(x).

Русский

Для любой функции f образ множества s — это множество y, для которого существует x ∈ s такой, что y ∈ f(x).

LaTeX

$$$f.image\\,s = \\{ y \\mid \\exists x \\in s,\\ y \\in f(x) \\}$$$

Lean4

theorem image_def (s : Set α) : f.image s = {y | ∃ x ∈ s, y ∈ f x} :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru