edgeDensity_nonneg

Mathlib.Combinatorics.SimpleGraph.Density

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

English

For any s and t, the edge density between s and t is nonnegative.

Русский

Для любых s и t плотность рёбер между ними неотрицательная.

LaTeX

$$0 ≤ G.edgeDensity s t$$

Lean4

theorem edgeDensity_nonneg (s t : Finset α) : 0 ≤ G.edgeDensity s t :=
  Rel.edgeDensity_nonneg _ _ _

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

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

Разделы

Аффилиация

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