trans_left_one

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Fin.cycleIcc.trans_left_one

← MathLib Explorer

English

If i ≤ j, then (cycleIcc j i) ∘ (cycleIcc i k) = cycleIcc i k.

Русский

Если i ≤ j, то (cycleIcc j i) ∘ (cycleIcc i k) = cycleIcc i k.

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i j k : \\mathrm{Fin}(n)},\\; i \\le j \\Rightarrow (\\mathrm{cycleIcc}(j,i) \\circ \\mathrm{cycleIcc}(i,k)) = \\mathrm{cycleIcc}(i,k)$$$

Lean4

theorem trans_left_one [NeZero n] (hij : i ≤ j) : (cycleIcc j i) ∘ (cycleIcc i k) = cycleIcc i k := by simp [hij]

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

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

Разделы

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

Аффилиация

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