mul_edgeDensity_le_edgeDensity — Mathlib

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

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