mem_range_toPermHom'_iff — Mathlib

English

For τ in Perm(g.cycleFactorsFinset), τ ∈ range_toPermHom'(g) iff ∀ c, #(τ c).val.support = #c.val.support.

Русский

Для τ ∈ Perm(g.cycleFactorsFinset), τ ∈ range_toPermHom'(g) тогда и только тогда, когда ∀ c выполняется #{(τ c).val.support} = #{c.val.support}.

LaTeX

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

Lean4

theorem mem_range_toPermHom'_iff {τ : Perm g.cycleFactorsFinset} :
    τ ∈ range_toPermHom' g ↔ ∀ c, #(τ c).val.support = #c.val.support :=
  Iff.rfl

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