graphOn_univ_inj

Mathlib.Data.Set.Function

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

English

The map that sends a function to its universal graph is injective: f ↦ univ.graphOn f is injective.

Русский

Отображение функций в их универсальные графы инъективно: f ↦ univ.graphOn f.

LaTeX

$$$\\text{Injective}(f \\mapsto \\mathrm{univ.graphOn}\,f).$$$

Lean4

theorem graphOn_univ_inj {g : α → β} : univ.graphOn f = univ.graphOn g ↔ f = g := by simp

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

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

Разделы

Аффилиация

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