isUniform_comm

Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

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

English

IsUniform is commutative in s and t: isUniform ε s t equals isUniform ε t s.

Русский

IsUniform коммутивное по отношению к s и t: равносильно isUniform ε t s.

LaTeX

$$IsUniform(G, ε, s, t) ↔ IsUniform(G, ε, t, s)$$

Lean4

theorem isUniform_comm : IsUniform G ε s t ↔ IsUniform G ε t s :=
  ⟨fun h => h.symm, fun h => h.symm⟩

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

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

Разделы

Аффилиация

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