interedges_empty_left

Mathlib.Combinatorics.SimpleGraph.Density

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

English

If the left set is empty, there are no interedges between it and any t.

Русский

Если левая часть пустая, между ней и любым t межрёбер нет.

LaTeX

$$G.interedges ∅ t = ∅$$

Lean4

@[simp]
theorem interedges_empty_left (t : Finset α) : G.interedges ∅ t = ∅ :=
  Rel.interedges_empty_left _

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

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

Разделы

Аффилиация

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