cycleType_extendDomain — Mathlib

English

ExtendDomain preserves cycleType (same as 124059).

Русский

ExtendDomain сохраняет cycleType.

LaTeX

$$$$\mathrm{cycleType}(g.\mathrmextendDomain f) = \mathrm{cycleType}(g).$$$$

Lean4

@[simp]
theorem cycleType_extendDomain {β : Type*} [Fintype β] [DecidableEq β] {p : β → Prop} [DecidablePred p]
    (f : α ≃ Subtype p) {g : Perm α} : cycleType (g.extendDomain f) = cycleType g := by
  induction g using cycle_induction_on with
  | base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
  | base_cycles σ hσ => rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
  | induction_disjoint σ τ hd _ hσ hτ =>
    rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]

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