graphOn_univ_eq_range

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.graphOn_univ_eq_range

English

The graph of f over the universal set equals the range of the map x ↦ (x, f(x)).

Русский

Граф функции f на всём множестве эквивалентен диапазону отображения x ↦ (x, f(x)).

LaTeX

$$$\operatorname{graphOn}(f, \mathsf{univ}) = \operatorname{range}(\lambda x. (x, f(x)))$$$

Lean4

theorem graphOn_univ_eq_range : univ.graphOn f = range fun x ↦ (x, f x) :=
  image_univ

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

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

Разделы

Аффилиация

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