trans_right_one

Mathlib.GroupTheory.Perm.Fin

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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