left_nonuniformWitnesses_subset

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

URI: https://scilib.ai/kg/mathlib#SimpleGraph.left_nonuniformWitnesses_subset

← MathLib Explorer

English

If G is not ε-uniform on s,t, then the right witness from the pair lies inside t.

Русский

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

LaTeX

$$(G.nonuniformWitnesses ε s t).snd ⊆ t$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru