range_toPermHom' — Mathlib

English

The range_toPermHom' g is defined as the subgroup of Perm(g.cycleFactorsFinset) consisting of all τ with ∀ c, #(τ c).val.support = #c.val.support.

Русский

range_toPermHom' g задаётся как подгруппа Perm(g.cycleFactorsFinset), состоящая из тех τ, для которых ∀ c выполняется #(τ c).val.support = #c.val.support.

LaTeX

$$$\operatorname{range\_toPermHom'}(g) = \{\tau \in \operatorname{Perm}(g.cycleFactorsFinset) \;|\; \forall c, #(\tau c).val.support = #c.val.support\}$$$

Lean4

/-- The range of `Equiv.Perm.OnCycleFactors.toPermHom`.

The equality is proved by `Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom'`. -/
def range_toPermHom' : Subgroup (Perm g.cycleFactorsFinset)
    where
  carrier := {τ | ∀ c, #(τ c).val.support = #c.val.support}
  one_mem' := by simp only [Set.mem_setOf_eq, coe_one, id_eq, imp_true_iff]
  mul_mem' hσ
    hτ := by
    simp only [Subtype.forall, Set.mem_setOf_eq, coe_mul, Function.comp_apply]
    simp only [Subtype.forall, Set.mem_setOf_eq] at hσ hτ
    intro c hc
    rw [hσ, hτ]
  inv_mem'
    hσ := by
    simp only [Subtype.forall, Set.mem_setOf_eq] at hσ ⊢
    intro c hc
    rw [← hσ]
    · simp only [Finset.coe_mem, Subtype.coe_eta, apply_inv_self]
    · simp only [Finset.coe_mem]

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