to_red

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.Red.Step.to_red

English

Every one-step reduction relation implies a sequence of reductions, i.e., a step implies a reduction.

Русский

Каждое одношаговое редукционное отношение порождает редукцию в виде последовательности редукций.

LaTeX

$$$\forall L_1,L_2:\, Step(L_1,L_2) \Rightarrow Red(L_1,L_2)$$$

Lean4

@[to_additive]
theorem to_red : Step L₁ L₂ → Red L₁ L₂ :=
  ReflTransGen.single

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

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

Разделы

Аффилиация

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