edgeDensity_empty_left

Mathlib.Combinatorics.SimpleGraph.Density

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

← MathLib Explorer

English

If the right set is empty, the edge density is zero.

Русский

Если правая часть пуста, плотность ребер равна нулю.

LaTeX

$$$\operatorname{edgeDensity}(r, s, \emptyset) = 0$$$

Lean4

@[simp]
theorem edgeDensity_empty_left (t : Finset β) : edgeDensity r ∅ t = 0 := by
  rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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