theorem RenamingSets.Ren.transfer_def {𝔸 : Type u_2} (A : Finset 𝔸) (σ₁ σ₂ : Ren 𝔸) : transfer A σ₁ σ₂ = { toFun := fun (a : 𝔸) => if h : ∃ b ∈ A, a = σ₁ b then σ₂ h.choose else a, exists_support' := ⋯ }

@[irreducible]

noncomputable def RenamingSets.Ren.transfer {𝔸 : Type u_2} (A : Finset 𝔸) (σ₁ σ₂ : Ren 𝔸) : Ren 𝔸

transfer A σ₁ σ₂ maps the outputs of σ₁ on A to the outputs of σ₂ on A, i.e., transfer A σ₁ σ₂ (σ₁ a) = σ₂ a (provided a ∈ A and σ₁ is injective on A.)

Equations

• RenamingSets.Ren.transfer A σ₁ σ₂ = { toFun := fun (a : 𝔸) => if h : ∃ b ∈ A, a = σ₁ b then σ₂ h.choose else a, exists_support' := ⋯ }

@[simp]

theorem RenamingSets.Ren.transfer_of_mem {𝔸 : Type u_1} {A : Finset 𝔸} {σ₁ σ₂ : Ren 𝔸} (hσ₁ : Set.InjOn ⇑σ₁ ↑A) {a : 𝔸} (ha : a ∈ A) : (transfer A σ₁ σ₂) (σ₁ a) = σ₂ a

@[simp]

theorem RenamingSets.Ren.transfer_of_notMem {𝔸 : Type u_1} {A : Finset 𝔸} {σ₁ σ₂ : Ren 𝔸} {a : 𝔸} (ha : ∀ x ∈ A, σ₁ x ≠ a) : (transfer A σ₁ σ₂) a = a