edgeDensity_le_one

Mathlib.Combinatorics.SimpleGraph.Density

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

English

The edge density between any s and t is at most 1.

Русский

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

LaTeX

$$G.edgeDensity s t ≤ 1$$

Lean4

theorem edgeDensity_le_one (s t : Finset α) : G.edgeDensity s t ≤ 1 :=
  Rel.edgeDensity_le_one _ _ _

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

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

Разделы

Аффилиация

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