graphOn

Mathlib.Data.Set.Operations

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

English

Let f: α → β and s ⊆ α. The graph of f on s is the set of pairs (x, f(x)) with x ∈ s.

Русский

Пусть f: α → β и s ⊆ α. График функции f на s — это множество пар (x, f(x)) при x ∈ s.

LaTeX

$$$\mathrm{graphOn}(f,s) = \{(x, f(x)) : x \in s\}$$$

Lean4

/-- The graph of a function `f : α → β` on a set `s`. -/
def graphOn (f : α → β) (s : Set α) : Set (α × β) :=
  (fun x ↦ (x, f x)) '' s

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

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

Разделы

Аффилиация

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