isAdjMatrix_adjMatrix

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

← MathLib Explorer

English

The adjacency matrix is itself an adjacency matrix.

Русский

Матрица смежности сама является матрицей смежности.

LaTeX

$$(G.adjMatrix\\, \\alpha).IsAdjMatrix$$

Lean4

/-- The adjacency matrix of `G` is an adjacency matrix. -/
@[simp]
theorem isAdjMatrix_adjMatrix [Zero α] [One α] : (G.adjMatrix α).IsAdjMatrix :=
  { zero_or_one := fun i j => by by_cases h : G.Adj i j <;> simp [h] }

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

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

Разделы

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

Аффилиация

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