mk_mem_graph

Mathlib.Data.Finsupp.Basic

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

English

If a is in the support of f, then (a, f(a)) is in f.graph.

Русский

Если элемент a принадлежит опоре функции f, то пара (a, f(a)) принадлежит графу f.

LaTeX

$$a \\in \\operatorname{supp}(f) \\Rightarrow (a, f(a)) \\in f.graph$$

Lean4

theorem mk_mem_graph (f : α →₀ M) {a : α} (ha : a ∈ f.support) : (a, f a) ∈ f.graph :=
  mk_mem_graph_iff.2 ⟨rfl, mem_support_iff.1 ha⟩

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

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

Разделы

Аффилиация

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