edgeDensity_empty_right

Mathlib.Combinatorics.SimpleGraph.Density

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

English

The density between s and the empty set is zero.

Русский

Плотность между s и пустым множеством равна нулю.

LaTeX

$$G.edgeDensity s ∅ = 0$$

Lean4

@[simp]
theorem edgeDensity_empty_right (s : Finset α) : G.edgeDensity s ∅ = 0 :=
  Rel.edgeDensity_empty_right _ _

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

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

Разделы

Аффилиация

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