one_lt_of_mem_cycleType

Mathlib.GroupTheory.Perm.Cycle.Type

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.one_lt_of_mem_cycleType

English

If n is in the cycle type, then 1 < n.

Русский

Если n ∈ cycleType(σ), то 1 < n.

LaTeX

$$$\forall \sigma : \mathrm{Perm}(\alpha), \forall n, n \in \sigma.\cycleType \Rightarrow 1 < n$$$

Lean4

theorem one_lt_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 1 < n :=
  two_le_of_mem_cycleType h

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

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

Разделы

Аффилиация

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