edge_self_eq_bot

Mathlib.Combinatorics.SimpleGraph.Operations

URI: https://scilib.ai/kg/mathlib#SimpleGraph.edge_self_eq_bot

English

The edge from a vertex to itself is the bottom relation: edge s s = ⊥.

Русский

Ребро от вершины к самой себе равно нижнему отношению: edge s s = ⊥.

LaTeX

$$$ \text{edge}(s,s) = \bot $$$

Lean4

@[simp]
theorem edge_self_eq_bot : edge s s = ⊥ := by ext; rw [edge_adj]; simp_all

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

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

Разделы

Аффилиация

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