nonuniformWitnesses — Mathlib

English

If G is not ε-uniform on s,t, then the left witness from the nonuniform witness pair lies inside s.

Русский

Если G не ε-однороден на s,t, левый свидетель пары неоднородности содержится в s.

LaTeX

$$(G.nonuniformWitnesses ε s t).fst ⊆ s$$

Lean4

/-- An arbitrary pair of subsets witnessing the non-uniformity of `(s, t)`. If `(s, t)` is uniform,
returns `(s, t)`. Witnesses for `(s, t)` and `(t, s)` don't necessarily match. See
`SimpleGraph.nonuniformWitness`. -/
noncomputable def nonuniformWitnesses (ε : 𝕜) (s t : Finset α) : Finset α × Finset α :=
  if h : ¬G.IsUniform ε s t then ((not_isUniform_iff.1 h).choose, (not_isUniform_iff.1 h).choose_spec.2.choose)
  else (s, t)

Похожие утверждения