graph

Mathlib.Data.Rel

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

Lean4

/-- The graph of a function as a relation. -/
def graph (f : α → β) : SetRel α β :=
  {(a, b) | f a = b}

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

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

Разделы

Аффилиация

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