edgeDensity_add_edgeDensity_compl

English

If s and t are nonempty and disjoint, the sum of edge density and complement edge density between s and t equals 1.

Русский

Если s и t непусты и несвязаны между собой, сумма плотности рёбер и плотности дополнения между s и t равна 1.

LaTeX

$$(s.Nonempty) ∧ (t.Nonempty) ∧ Disjoint s t → G.edgeDensity s t + G^complement.edgeDensity s t = 1$$

Lean4

theorem edgeDensity_add_edgeDensity_compl (hs : s.Nonempty) (ht : t.Nonempty) (h : Disjoint s t) :
    G.edgeDensity s t + Gᶜ.edgeDensity s t = 1 :=
  by
  rw [edgeDensity_def, edgeDensity_def, ← add_div, div_eq_one_iff_eq]
  · exact mod_cast card_interedges_add_card_interedges_compl _ h
  · positivity

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