nonuniformWitness_mem_nonuniformWitnesses

English

If s and t are not uniform and t is a part of P, then the witness G.nonuniformWitness ε s t lies in P.nonuniformWitnesses G ε s.

Русский

Если s и t не однородны и t является частью разбиения P, то свидетель неоднородности G.nonuniformWitness ε s t принадлежит P.nonuniformWitnesses G ε s.

LaTeX

$$¬G.IsUniform(ε, s, t) ∧ t ∈ P.parts ∧ s ≠ t ⇒ G.nonuniformWitness ε s t ∈ P.nonuniformWitnesses G ε s$$

Lean4

theorem nonuniformWitness_mem_nonuniformWitnesses (h : ¬G.IsUniform ε s t) (ht : t ∈ P.parts) (hst : s ≠ t) :
    G.nonuniformWitness ε s t ∈ P.nonuniformWitnesses G ε s :=
  mem_image_of_mem _ <| mem_filter.2 ⟨ht, hst, h⟩

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