two_le_of_mem_cycleType — Mathlib

English

If n is in the cycle type of σ, then n ≥ 2.

Русский

Если n принадлежит cycleType(σ), то n ≥ 2.

LaTeX

$$$\forall \sigma : \mathrm{Perm}(\alpha), \forall n, n \in \sigma.\mathrmcycleType \Rightarrow 2 \le n$$$

Lean4

theorem two_le_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 2 ≤ n :=
  by
  simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map, mem_cycleFactorsFinset_iff] at h
  obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h
  exact hc.two_le_card_support

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