cycleType_le_of_mem_cycleFactorsFinset

English

Extending the domain via an equivalence with a subtype does not change the cycle-type.

Русский

Расширение области определения через эквивалентность с подтипом не изменяет cycleType.

LaTeX

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

Lean4

theorem cycleType_le_of_mem_cycleFactorsFinset {f g : Perm α} (hf : f ∈ g.cycleFactorsFinset) :
    f.cycleType ≤ g.cycleType := by
  have hf' := mem_cycleFactorsFinset_iff.1 hf
  rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]
  refine map_le_map ?_
  simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf

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