interedges_empty_left

Mathlib.Combinatorics.SimpleGraph.Density

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

English

If the left vertex set is empty, interedges is the empty set.

Русский

Если левое множество вершин пусто, interedges равно пустому множеству.

LaTeX

$$$ \mathrm{interedges}(r, \emptyset, t) = \emptyset $$$

Lean4

@[simp]
theorem interedges_empty_left (t : Finset β) : interedges r ∅ t = ∅ := by
  rw [interedges, Finset.empty_product, filter_empty]

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

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

Разделы

Аффилиация

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