nonuniformWitness_subset — Mathlib

English

If not ε-uniform, then the left witness lies inside s and the right witness lies inside t.

Русский

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

LaTeX

$$G.nonuniformWitness ε s t ⊆ s ∧ G.nonuniformWitness ε s t ⊆ t$$

Lean4

theorem nonuniformWitness_subset (h : ¬G.IsUniform ε s t) : G.nonuniformWitness ε s t ⊆ s :=
  by
  unfold nonuniformWitness
  split_ifs
  · exact G.left_nonuniformWitnesses_subset h
  · exact G.right_nonuniformWitnesses_subset fun i => h i.symm

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