pathGraph_two_eq_top

Mathlib.Combinatorics.SimpleGraph.Hasse

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

← MathLib Explorer

English

The path graph on two vertices is the top element (complete graph).

Русский

Граф пути на двух вершинах равен верхнему элементу (полный граф).

LaTeX

$$$pathGraph 2 = ⊤$$$

Lean4

theorem pathGraph_two_eq_top : pathGraph 2 = ⊤ := by
  ext u v
  fin_cases u <;> fin_cases v <;> simp [pathGraph, ← Fin.coe_covBy_iff, covBy_iff_add_one_eq]

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

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

Разделы

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

Аффилиация

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