𝕜 : Type ?u.115961
ι : Type ?u.115964
κ : Type ?u.115967
α : Type u_1
β : Type ?u.115973
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card (interedges G s t)) + ↑(card (interedges (Gᶜ) s t)) = ↑(card s) * ↑(card t)

𝕜 : Type ?u.115961
ι : Type ?u.115964
κ : Type ?u.115967
α : Type u_1
β : Type ?u.115973
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card s) * ↑(card t) ≠ 0
𝕜 : Type ?u.115961
ι : Type ?u.115964
κ : Type ?u.115967
α : Type u_1
β : Type ?u.115973
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ edgeDensity G s t + edgeDensity (Gᶜ) s t = 1
rw [edgeDensity_def, edgeDensity_def, div_add_div_same, div_eq_one_iff_eq]
no goals
𝕜 : Type ?u.115961
ι : Type ?u.115964
κ : Type ?u.115967
α : Type u_1
β : Type ?u.115973
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card (interedges G s t)) + ↑(card (interedges (Gᶜ) s t)) = ↑(card s) * ↑(card t)
exact_mod_cast card_interedges_add_card_interedges_compl _ h
no goals
𝕜 : Type ?u.115961
ι : Type ?u.115964
κ : Type ?u.115967
α : Type u_1
β : Type ?u.115973
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
hs : Finset.Nonempty s
ht : Finset.Nonempty t
h : Disjoint s t
⊢ ↑(card s) * ↑(card t) ≠ 0
apply mul_ne_zero <;> exact_mod_cast Nat.pos_iff_ne_zero.1 (Nonempty.card_pos ‹_›)