edgeSet_subset_setOf_not_isDiag

Mathlib.Combinatorics.SimpleGraph.Basic

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

← MathLib Explorer

English

All edges of G are non-diagonal.

Русский

Все ребра графа G не диагональны.

LaTeX

$$$$ E(G) \subseteq \{ e \mid \neg e.IsDiag \}. $$$$

Lean4

@[simp]
theorem edgeSet_subset_setOf_not_isDiag : G.edgeSet ⊆ {e | ¬e.IsDiag} := fun _ h =>
  (Sym2.fromRel_irreflexive (sym := G.symm)).mp G.loopless h

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

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

Разделы

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

Аффилиация

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