theorem RenamingSets.Ren.base_def {𝔸 : Type u_2} (A : Finset 𝔸) (σ : Ren 𝔸) : base A σ = { toFun := fun (a : 𝔸) => if h : a ∈ A then have this := ⋯; this.choose else a, exists_support' := ⋯ }

@[irreducible]

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

Every renaming σ has a "base" renaming base σ such that σ * base σ = σ and σ (base σ a) = σ (base σ b) ↔ base σ a = base σ b.

Equations

• RenamingSets.Ren.base A σ = { toFun := fun (a : 𝔸) => if h : a ∈ A then have this := ⋯; this.choose else a, exists_support' := ⋯ }

@[simp]

theorem RenamingSets.Ren.coe_base {𝔸 : Type u_1} (A : Finset 𝔸) (σ : Ren 𝔸) (a : 𝔸) : σ ((base A σ) a) = σ a

@[simp]

theorem RenamingSets.Ren.mul_base {𝔸 : Type u_1} (A : Finset 𝔸) (σ : Ren 𝔸) : σ * base A σ = σ

@[simp]

theorem RenamingSets.Ren.mul_base_r {𝔸 : Type u_1} (A : Finset 𝔸) (σ σ' : Ren 𝔸) : σ * (base A σ * σ') = σ * σ'

@[simp]

theorem RenamingSets.Ren.base_idem {𝔸 : Type u_1} (A : Finset 𝔸) (σ : Ren 𝔸) (a : 𝔸) : (base A σ) ((base A σ) a) = (base A σ) a

@[simp]

theorem RenamingSets.Ren.base_idem' {𝔸 : Type u_1} (A : Finset 𝔸) (σ : Ren 𝔸) : base A σ * base A σ = base A σ

@[simp]

theorem RenamingSets.Ren.base_of_mem {𝔸 : Type u_1} (A : Finset 𝔸) (σ : Ren 𝔸) (a : 𝔸) : (base A σ) a ∈ A ↔ a ∈ A

@[simp]

theorem RenamingSets.Ren.base_of_notMem {𝔸 : Type u_1} (σ : Ren 𝔸) {A : Finset 𝔸} {a : 𝔸} (ha : a ∉ A) : (base A σ) a = a

theorem RenamingSets.Ren.base_eq_iff {𝔸 : Type u_1} {a b : 𝔸} (A : Finset 𝔸) (ha : a ∈ A) (hb : b ∈ A) (σ : Ren 𝔸) : (base A σ) a = (base A σ) b ↔ σ a = σ b