mgraph_eq_mrange_prod

Mathlib.Algebra.Group.Graph

URI: https://scilib.ai/kg/mathlib#MonoidHom.mgraph_eq_mrange_prod

English

The graph of f is exactly the image of the map g ↦ (g, f(g)) from G to G × H.

Русский

Граф графа f равен образом отображения g ↦ (g, f(g)) из G в G × H.

LaTeX

$$$f.mgraph = \\operatorname{mrange}((\\mathrm{id}_G) \\! .prod f) = \\{(g, f(g)) \\mid g \\in G\\}.$$$

Lean4

@[to_additive mgraph_eq_mrange_prod]
theorem mgraph_eq_mrange_prod (f : G →* H) : f.mgraph = mrange ((id _).prod f) := by aesop

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

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

Разделы

Аффилиация

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