length_le

Mathlib.GroupTheory.FreeGroup.Basic

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

English

For any L1, L2 with a Step relation, the size (sizeOf) of L2 is strictly smaller than that of L1.

Русский

Для любых L1, L2 со связью Step размер L2strictly меньше размера L1.

LaTeX

$$$\text{Step}\,L_1\,L_2 \Rightarrow \text{sizeOf}(L_2) < \text{sizeOf}(L_1)$$$

Lean4

@[to_additive]
theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length :=
  h.sublist.length_le

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

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

Разделы

Аффилиация

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