edgeFinset_nonempty

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

A graph has a nonempty edgeFinset iff it is not the bottom graph.

Русский

edgeFinset непустое ⇔ граф не равен нижнему графу.

LaTeX

$$$G.edgeFinset.Nonempty \\iff G \\ne \\bot$$$

Lean4

theorem edgeFinset_nonempty : G.edgeFinset.Nonempty ↔ G ≠ ⊥ := by
  rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]

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

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

Разделы

Аффилиация

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