nonempty_of_not_uniform

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

URI: https://scilib.ai/kg/mathlib#Finpartition.nonempty_of_not_uniform

English

If P is not uniform with respect to G at ε, then P.parts is nonempty.

Русский

Если P не однородно относительно G на масштабе ε, то P.parts непусто.

LaTeX

$$¬P.IsUniform(G,ε) ⇒ P.parts ≠ ∅$$

Lean4

theorem nonempty_of_not_uniform (h : ¬P.IsUniform G ε) : P.parts.Nonempty :=
  nonempty_of_ne_empty fun h₁ => h <| isUniformOfEmpty h₁

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

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

Разделы

Аффилиация

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