English
If ε ≤ ε' and a graph is ε-uniform on s,t, then it is ε'-uniform on s,t as well.
Русский
Если ε ≤ ε' и граф является ε-однородным на s,t, то он также является ε'-однородным на s,t.
LaTeX
$$$\\forall s',\\; s'\\subseteq s \\;\\to\\; \\forall t'\\;\\subseteq t,\\; (|s'| \\cdot ε' ≤ |s'|) \\land (|t'| \\cdot ε' ≤ |t'|) \\Rightarrow |G.edgeDensity(s',t') - G.edgeDensity(s,t)| < ε'$$$
Lean4
/-- A pair of finsets of vertices is `ε`-uniform (aka `ε`-regular) iff their edge density is close
to the density of any big enough pair of subsets. Intuitively, the edges between them are
random-like. -/
def IsUniform (s t : Finset α) : Prop :=
∀ ⦃s'⦄,
s' ⊆ s →
∀ ⦃t'⦄,
t' ⊆ t → (#s : 𝕜) * ε ≤ #s' → (#t : 𝕜) * ε ≤ #t' → |(G.edgeDensity s' t' : 𝕜) - (G.edgeDensity s t : 𝕜)| < ε
