α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < ε
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ abs (↑(edgeDensity G t' s') - ↑(edgeDensity G t s)) < ε
rw [edgeDensity_comm _ t', edgeDensity_comm _ t]
no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < ε
exact h hs' ht' hs ht