right_nonuniformWitnesses_card — Mathlib

English

If not ε-uniform, then the pair (s,t) is contained among the nonuniform pairs with witness bounds.

Русский

Если не существует ε-однородности, то пара (s,t) участвует в наборе неоднородных пар с ограничениями по свидетелям.

LaTeX

$$G.IsUniform ε s t = false ⇒ (s,t) ∈ G.nonUniforms ε$$

Lean4

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

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