not_isDiag_of_mem_edgeFinset

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

Every edge contained in edgeFinset is non-diagonal (non-loops).

Русский

Каждое ребро в edgeFinset не является петлей (не диагональное).

LaTeX

$$$e \\in G.edgeFinset \\Rightarrow ¬e.\\\\IsDiag$$$

Lean4

theorem not_isDiag_of_mem_edgeFinset : e ∈ G.edgeFinset → ¬e.IsDiag :=
  not_isDiag_of_mem_edgeSet _ ∘ mem_edgeFinset.1

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

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

Разделы

Аффилиация

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