theorem RenamingSets.Function.ext' {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [DecidableEq 𝔸] (A : Finset 𝔸) {f : X → Y} (hf : IsSupportOfF A f) {g : X → Y} (hg : IsSupportOfF A g) (hA : ∀ (x : X), supp 𝔸 x ∩ A = ∅ → f x = g x) : f = g

noncomputable instance RenamingSets.Function.instRenameActionForall {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] : RenameAction 𝔸 (X → Y)

Equations

• One or more equations did not get rendered due to their size.

theorem RenamingSets.Function.rename_def {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) (f : X → Y) (a✝ : X) : rename σ f a✝ = (if hf : IsSupportedF 𝔸 f then (PartialHom.rename σ ⋯).extend else f) a✝

theorem RenamingSets.Function.isSupportOfF_rename {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] {A : Finset 𝔸} (σ : Ren 𝔸) (hσ₁ : σ.supp ⊆ A) (hσ₂ : ∀ a ∈ A, σ a ∈ A) {f : X → Y} (hf : IsSupportOfF A f) : IsSupportOfF A (rename σ f)

@[simp]

theorem RenamingSets.Function.isSupportedF_rename {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) (f : X → Y) : IsSupportedF 𝔸 (rename σ f) ↔ IsSupportedF 𝔸 f

theorem RenamingSets.Function.isSupportedF_rename' {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) {f : X → Y} (hf : IsSupportedF 𝔸 f) : IsSupportedF 𝔸 (rename σ f)

@[simp]

theorem RenamingSets.Function.rename_apply {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) {f : X → Y} (hf : IsSupportedF 𝔸 f) (x : X) : rename σ f (rename σ x) = rename σ (f x)

@[simp]

theorem RenamingSets.Function.rename_apply' {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (σ : Ren 𝔸) {f : X → Y} (hf : ¬IsSupportedF 𝔸 f) : rename σ f = f

@[simp]

theorem RenamingSets.Function.isSupportOf_of_isSupportOfF {𝔸 : Type u_1} [Infinite 𝔸] {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {Y : Type u_3} [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (A : Finset 𝔸) (f : X → Y) (hf : IsSupportOfF A f) : IsSupportOf A f