mono

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsUniform.mono

← MathLib Explorer

English

There exists a decision procedure for IsUniform with fixed ε.

Русский

Существет процедура принятия решения для IsUniform при фиксированном ε.

LaTeX

$$DecidableRel (G.IsUniform ε)$$

Lean4

theorem mono {ε' : 𝕜} (h : ε ≤ ε') (hε : IsUniform G ε s t) : IsUniform G ε' s t := fun s' hs' t' ht' hs ht => by
  refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h <;> gcongr

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

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

Разделы

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

Аффилиация

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