noncomputable def RenamingSets.Ren.fresh {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) : Ren 𝔸

fresh A B is a renaming which assigns a unique name for every a ∈ A, such that a ∉ B. Names not in A are left alone (i.e. a ∉ A → fresh A B a = a).

Equations

• RenamingSets.Ren.fresh A B = { toFun := ⋯.choose, exists_support' := ⋯ }

@[simp]

theorem RenamingSets.Ren.fresh_injOn {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) : Set.InjOn ⇑(fresh A B) ↑A

theorem RenamingSets.Ren.fresh_injOn' {𝔸 : Type u_1} [Infinite 𝔸] {A B : Finset 𝔸} {a b : 𝔸} (ha : a ∈ A) (hb : b ∈ A) (h : (fresh A B) a = (fresh A B) b) : a = b

theorem RenamingSets.Ren.fresh_of_mem {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) (a : 𝔸) : a ∈ A → (fresh A B) a ∉ B

theorem RenamingSets.Ren.fresh_of_mem' {𝔸 : Type u_1} [Infinite 𝔸] (A B C : Finset 𝔸) (a : 𝔸) : a ∈ A → C ⊆ B → (fresh A B) a ∉ C

noncomputable def RenamingSets.Ren.unfresh {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) : Ren 𝔸

The inverse renaming for fresh.

Equations

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

theorem RenamingSets.Ren.unfresh_coe {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) (a : 𝔸) : (unfresh A B) a = if h : ∃ b ∈ A, (fresh A B) b = a then h.choose else a

@[simp]

theorem RenamingSets.Ren.unfresh_of_mem {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) (a : 𝔸) : a ∈ B → (unfresh A B) a = a

theorem RenamingSets.Ren.unfresh_of_not_fresh {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) (a : 𝔸) : (∀ b ∈ A, a ≠ (fresh A B) b) → (unfresh A B) a = a

@[simp]

theorem RenamingSets.Ren.unfresh_fresh₁ {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) (a : 𝔸) : a ∈ A → (unfresh A B) ((fresh A B) a) = a

@[simp]

theorem RenamingSets.Ren.unfresh_fresh₂ {𝔸 : Type u_1} [Infinite 𝔸] (A B : Finset 𝔸) (a : 𝔸) : a ∈ B → (unfresh A B) ((fresh A B) a) = a