nonUniforms_mono

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

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

← MathLib Explorer

English

If P.IsUniform for ε and ε ≤ ε', then P.IsUniform for ε'.

Русский

Если P является ε-однородным и ε ≤ ε', то P является ε'-однородным.

LaTeX

$$P.IsUniform G ε ∧ ε ≤ ε' ⇒ P.IsUniform G ε'$$

Lean4

theorem nonUniforms_mono {ε ε' : 𝕜} (h : ε ≤ ε') : P.nonUniforms G ε' ⊆ P.nonUniforms G ε :=
  monotone_filter_right _ fun _ => mt <| SimpleGraph.IsUniform.mono h

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

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

Разделы

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

Аффилиация

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