left_nonuniformWitnesses_card — Mathlib

English

If not ε-uniform, then ε·|s| ≤ |W1|, where W1 is the left witness.

Русский

Если не существует ε-однородности, то ε·|s| ≤ |W1|, где W1 — левый свидетель.

LaTeX

$$#s * ε ≤ # (G.nonuniformWitness ε s t).fst$$

Lean4

theorem left_nonuniformWitnesses_card (h : ¬G.IsUniform ε s t) : #s * ε ≤ #(G.nonuniformWitnesses ε s t).1 :=
  by
  rw [nonuniformWitnesses, dif_pos h]
  exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1

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