sound

Mathlib.GroupTheory.FreeGroup.Reduce

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\mathrm{Red}.\mathrm{enum}\;\mathrm{sound} : L_2 \in \mathrm{List.filter}(\mathrm{Red} L_1)(\mathrm{List.sublists} L_1) \Rightarrow \mathrm{Red} L_1 L_2$$$

Lean4

theorem sound (H : L₂ ∈ List.filter (Red L₁) (List.sublists L₁)) : Red L₁ L₂ :=
  of_decide_eq_true (@List.of_mem_filter _ _ L₂ _ H)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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