α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t →
              ↑(card s) * ε ≤ ↑(card s') →
                ↑(card t) * ε ≤ ↑(card t') → abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < ε) ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧
              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑(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 : α
⊢ ¬IsUniform G ε s t ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧
              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))
unfold IsUniform
no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t →
              ↑(card s) * ε ≤ ↑(card s') →
                ↑(card t) * ε ≤ ↑(card t') → abs (↑(edgeDensity G s' t') - ↑(edgeDensity G s t)) < ε) ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧
              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))
simp only [not_forall, not_lt, exists_prop, exists_and_left, Rat.cast_abs, Rat.cast_sub]