English
If i ≤ j, then the cycleIcc(j,i) is the identity and has zero cycle length.
Русский
Если i ≤ j, то cycleIcc(j,i) — тождественная перестановка и имеет нулевую длину цикла.
LaTeX
$$$\\forall {n : \\mathbb{N}} \\; \\forall {i,j : \\mathrm{Fin}(n)}, i \\le j \\Rightarrow \\mathrm{cycleIcc}(j,i) = 1 \\wedge \\mathrm{cycleIcc}(j,i).\\mathrm{cycleType} = \\emptyset$$$
Lean4
theorem isConj_of_support_equiv (f : { x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
(hf : ∀ (x : α) (hx : x ∈ (σ.support : Set α)), (f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
IsConj σ τ := by
refine isConj_iff.2 ⟨Equiv.extendSubtype f, ?_⟩
rw [mul_inv_eq_iff_eq_mul]
ext x
simp only [Perm.mul_apply]
by_cases hx : x ∈ σ.support
· rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
· exact hf x (Finset.mem_coe.2 hx)
·
rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
Classical.not_not.1 ((not_congr mem_support).mp hx)]
