graph

Mathlib.Data.PFun

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

← MathLib Explorer

English

The graph of a partial function f is the set of pairs (x, y) with y ∈ f(x).

Русский

Граф частичной функции f — множество пар (x, y) таких, что y ∈ f(x).

LaTeX

$$$\\mathrm{graph}(f) = \\{ (x,y) \\mid y \\in f(x)\\}$$$

Lean4

/-- Graph of a partial function `f` as the set of pairs `(x, f x)` where `x` is in the domain of
`f`. -/
def graph (f : α →. β) : Set (α × β) :=
  {p | p.2 ∈ f p.1}

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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