join_red_of_step

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.join_red_of_step

English

From a single-step reduction, obtain a join relation: Join Red L1 L2.

Русский

Из одного шага редукции получается отношение соединения: Join Red L1 L2.

LaTeX

$$$\text{Join}(\text{Red})(L_1,L_2)$$$

Lean4

@[to_additive]
theorem join_red_of_step (h : Red.Step L₁ L₂) : Join Red L₁ L₂ :=
  join_of_single reflexive_reflTransGen h.to_red

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

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

Разделы

Аффилиация

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