cycleType_of_card_le_mem_cycleType_add_two

English

If f^n is a cycle and the support of f is contained in the support of f^n, then f is a cycle.

Русский

Если f^n — цикл и опора f принадлежит опоре f^n, то f — цикл.

LaTeX

$${(f^n) \text{ is a cycle}} \wedge {\operatorname{supp}(f) \subseteq \operatorname{supp}(f^n)} \Rightarrow f \text{ is a cycle}$$

Lean4

theorem cycleType_of_card_le_mem_cycleType_add_two {n : ℕ} {g : Perm α} (hn2 : Fintype.card α < n + 2)
    (hng : n ∈ g.cycleType) : g.cycleType = { n } :=
  by
  obtain ⟨c, g', rfl, hd, hc, rfl⟩ := mem_cycleType_iff.1 hng
  suffices g'1 : g' = 1 by rw [hd.cycleType_mul, hc.cycleType, g'1, cycleType_one, add_zero]
  contrapose! hn2 with g'1
  apply le_trans _ (c * g').support.card_le_univ
  rw [hd.card_support_mul]
  exact add_le_add_left (two_le_card_support_of_ne_one g'1) _

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