mem_graph

Mathlib.Data.Rel

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

English

For any function f, a is related to b by the graph of f if and only if f(a) = b.

Русский

Для любой функции f, отношение a графа f держится тогда и только тогда, когда f(a) = b.

LaTeX

$$$a ~[f.graph] b \iff f(a) = b$$$

Lean4

@[simp]
theorem mem_graph : a ~[f.graph] b ↔ f a = b :=
  .rfl

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

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

Разделы

Аффилиация

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