α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * 1 ≤ ↑(card s')
ht : ↑(card t) * 1 ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < 1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ IsUniform G 1 s t
intro s' hs' t' ht' hs ht
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < 1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * 1 ≤ ↑(card s')
ht : ↑(card t) * 1 ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < 1
rw [mul_one] at hs ht
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ 0 < 1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < 1
rw [eq_of_subset_of_card_le hs' (Nat.cast_le.1 hs),
  eq_of_subset_of_card_le ht' (Nat.cast_le.1 ht), sub_self, abs_zero]
no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ 0 < 1
exact zero_lt_one