α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(card {a}) * ε ≤ ↑(card s')
ht : ↑(card {b}) * ε ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})) < ε
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
⊢ IsUniform G ε {a} {b}
intro s' hs' t' ht' hs ht
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(card s')
ht : ε ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})) < ε
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(card {a}) * ε ≤ ↑(card s')
ht : ↑(card {b}) * ε ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})) < ε
rw [card_singleton, Nat.cast_one, one_mul] at hs ht
case inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})) < ε

case inr
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
⊢ abs (↑(edgeDensity G {a} t') - ↑(edgeDensity G {a} {b})) < ε
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(card s')
ht : ε ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})) < ε
obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'
case inr.inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})) < ε

case inr.inr
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(card {b})
⊢ abs (↑(edgeDensity G {a} {b}) - ↑(edgeDensity G {a} {b})) < ε
case inr
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
⊢ abs (↑(edgeDensity G {a} t') - ↑(edgeDensity G {a} {b})) < ε
obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'
case inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ 0
⊢ abs (↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})) < ε
case inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})) < ε
replace hs : ε ≤ 0 := by simpa using hs
no goals
case inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ 0
⊢ abs (↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})) < ε
exact (hε.not_le hs).elim
no goals
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ ε ≤ 0
simpa using hs
case inr.inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ 0
⊢ abs (↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})) < ε
case inr.inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ abs (↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})) < ε
replace ht : ε ≤ 0 := by simpa using ht
no goals
case inr.inl
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ 0
⊢ abs (↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})) < ε
exact (hε.not_le ht).elim
no goals
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ ε ≤ 0
simpa using ht
no goals
case inr.inr
α : Type u_2
𝕜 : Type u_1
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(card {b})
⊢ abs (↑(edgeDensity G {a} {b}) - ↑(edgeDensity G {a} {b})) < ε
rwa [sub_self, abs_zero]