edgeDensity_comm — Mathlib

English

If r is symmetric, then edgeDensity(r,s,t) = edgeDensity(r,t,s).

Русский

Если r симметрична, то плотность ребер между s и t равна плотности между t и s.

LaTeX

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

Lean4

theorem edgeDensity_comm (hr : Symmetric r) (s t : Finset α) : edgeDensity r s t = edgeDensity r t s := by
  rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]

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