mem_range_toPermHom_iff' — Mathlib

English

A variant of membership in range: τ ∈ range iff the two compositions with τ coincide pointwise, i.e., the map compositions agree on all cycle factors.

Русский

Вариантность членства в образе: τ ∈ range тогда и только тогда, когда две композиции с τ совпадают на всех факторах цикла.

LaTeX

$$$τ ∈ (toPermHom g).range' \\iff (\\text{...})$$$

Lean4

/-- Unapplied variant of `Equiv.Perm.mem_range_toPermHom_iff` -/
theorem mem_range_toPermHom_iff' {τ} :
    τ ∈ (toPermHom g).range ↔
      (fun (c : g.cycleFactorsFinset) ↦ #c.val.support) ∘ τ = fun (c : g.cycleFactorsFinset) ↦ #c.val.support :=
  by
  rw [mem_range_toPermHom_iff, funext_iff]
  simp only [Subtype.forall, Function.comp_apply]

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