le_card_support_of_mem_cycleType

Mathlib.GroupTheory.Perm.Cycle.Type

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

← MathLib Explorer

English

If n is in the cycle-type of σ, then n is at most the size of σ's support.

Русский

Если n ∈ cycleType(σ), то n ≤ |σ|.support.

LaTeX

$$$$ n \in \mathrm{cycleType}(\sigma) \implies n \le |\sigma.\mathrm{support}|. $$$$

Lean4

theorem le_card_support_of_mem_cycleType {n : ℕ} {σ : Perm α} (h : n ∈ cycleType σ) : n ≤ #σ.support :=
  (le_sum_of_mem h).trans (le_of_eq σ.sum_cycleType)

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

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

Разделы

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

Аффилиация

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