right_nonuniformWitnesses_subset — Mathlib

English

If not ε-uniform, then ε·|t| ≤ |W2|, where W2 is the right witness.

Русский

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

LaTeX

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

Lean4

theorem right_nonuniformWitnesses_subset (h : ¬G.IsUniform ε s t) : (G.nonuniformWitnesses ε s t).2 ⊆ t :=
  by
  rw [nonuniformWitnesses, dif_pos h]
  exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.1

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