apply_eq_of_mem_graph

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.apply_eq_of_mem_graph

English

From a membership in the graph, obtain equality f(a)=m.

Русский

По принадлежности к графу можно получить равенство $f(a)=m$.

LaTeX

$$$\\text{If } (a,m) \\in f.graph, \\; \\text{then } f(a)=m$$$

Lean4

theorem apply_eq_of_mem_graph {a : α} {m : M} {f : α →₀ M} (h : (a, m) ∈ f.graph) : f a = m :=
  (mem_graph_iff.1 h).1

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

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

Разделы

Аффилиация

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