complete

Mathlib.GroupTheory.FreeGroup.Reduce

URI: https://scilib.ai/kg/mathlib#FreeGroup.Red.enum.complete

English

If Red L1 L2 holds, then L2 belongs to Red.enum L1.

Русский

Если Red L1 L2, тогда L2 принадлежит Red.enum L1.

LaTeX

$$$\mathrm{Red}.\mathrm{enum} \;\mathrm{complete} : \mathrm{Red} L_1 L_2 \Rightarrow L_2 \in \mathrm{FreeGroup.Red.enum}(L_1)$$$

Lean4

theorem complete (H : Red L₁ L₂) : L₂ ∈ Red.enum L₁ :=
  List.mem_filter_of_mem (List.mem_sublists.2 <| Red.sublist H) (decide_eq_true H)

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

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

Разделы

Аффилиация

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