notMem_graph_snd_zero

Mathlib.Data.Finsupp.Basic

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

← MathLib Explorer

English

The pair (a,0) is not in the graph of f.

Русский

Пара $(a,0)$ не принадлежит графу функции f.

LaTeX

$$$(a,0) \\notin f.graph$$$

Lean4

@[simp 1100] -- Higher priority shortcut instance for `mem_graph_iff`.

theorem notMem_graph_snd_zero (a : α) (f : α →₀ M) : (a, (0 : M)) ∉ f.graph := fun h => (mem_graph_iff.1 h).2.irrefl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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