English
Equality of interedges cardinality with partitions on the right side.
Русский
Эквивалентность кардинала ребер между s и t с разбиениями справа.
LaTeX
$$$\#(\operatorname{interedges}(r, s, t)) = \sum_{b \in P.parts} \#(\operatorname{interedges}(r, s, b))$$$
Lean4
theorem mul_edgeDensity_le_edgeDensity (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
(#s₂ : ℚ) / #s₁ * (#t₂ / #t₁) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁ :=
by
have hst : (#s₂ : ℚ) * #t₂ ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]
rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel₀ hst]
gcongr
exact interedges_mono hs ht