edgeDensity_nonneg

Mathlib.Combinatorics.SimpleGraph.Density

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

English

The edge density between any two finite sets is nonnegative.

Русский

Плотность ребер между любыми двумя конечными множествами неотрицательна.

LaTeX

$$$0 \le \operatorname{edgeDensity}(r, s, t)$$$

Lean4

theorem edgeDensity_nonneg (s : Finset α) (t : Finset β) : 0 ≤ edgeDensity r s t := by
  apply div_nonneg <;> exact mod_cast Nat.zero_le _

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

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

Разделы

Аффилиация

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