ofLE_refl

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Copy.ofLE_refl

English

For any graph G, the embedding of G into itself via the identity relation is the identity embedding: ofLE G G le_rfl = id G.

Русский

Для любого графа G вложение G в G через тождество равно тождественному вложению: ofLE G G le_rfl = id G.

LaTeX

$$$\text{ofLE } G\ G\; \mathrm{le\_rfl} = \mathrm{id\}G$$$

Lean4

@[simp]
theorem ofLE_refl : ofLE G G le_rfl = id G := by ext; simp

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

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

Разделы

Аффилиация

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