instance RenamingSets.Finset.instRenameActionFinsetOfDecidableEq {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] : RenameAction 𝔸 (Finset X)

Equations

• RenamingSets.Finset.instRenameActionFinsetOfDecidableEq = { rename := fun (σ : RenamingSets.Ren 𝔸) => Finset.image (RenamingSets.rename σ), rename_one := ⋯, rename_mul := ⋯ }

theorem RenamingSets.Finset.rename_def {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] (σ : Ren 𝔸) (s : Finset X) : rename σ s = Finset.image (rename σ) s

@[simp]

theorem RenamingSets.Finset.mem_rename {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] (x : X) (σ : Ren 𝔸) (xs : Finset X) : x ∈ rename σ xs ↔ ∃ x' ∈ xs, rename σ x' = x

@[simp]

theorem RenamingSets.Finset.isSupportOf_empty {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] (A : Finset 𝔸) : IsSupportOf A ∅

@[simp]

theorem RenamingSets.Finset.isSupported_empty {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] : IsSupported 𝔸 ∅

theorem RenamingSets.Finset.isSupportOf_insert {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] {A : Finset 𝔸} {x : X} {xs : Finset X} (hx : IsSupportOf A x) (hxs : IsSupportOf A xs) : IsSupportOf A (insert x xs)

theorem RenamingSets.Finset.isSupported_insert {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] {x : X} {xs : Finset X} (hx : IsSupported 𝔸 x) (hxs : IsSupported 𝔸 xs) : IsSupported 𝔸 (insert x xs)

theorem RenamingSets.Finset.rename_mono {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq X] (σ : Ren 𝔸) : Monotone (rename σ)

instance RenamingSets.Finset.instRenamingSetFinset {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [DecidableEq X] : RenamingSet 𝔸 (Finset X)

@[simp]

theorem RenamingSets.Finset.supp_empty {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [DecidableEq X] : supp 𝔸 ∅ = ∅

theorem RenamingSets.supp_rename_subset {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] [DecidableEq 𝔸] (σ : Ren 𝔸) (x : X) : supp 𝔸 (rename σ x) ⊆ rename σ (supp 𝔸 x)

theorem RenamingSets.supp_rename_subset' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] (σ : Ren 𝔸) (x : X) (a : 𝔸) : a ∈ supp 𝔸 (rename σ x) → ∃ b ∈ supp 𝔸 x, σ b = a

@[simp]

theorem RenamingSets.supp_rename {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] [DecidableEq 𝔸] (σ : Ren 𝔸) (x : X) (hσ : Set.InjOn ⇑σ ↑(supp 𝔸 x)) : supp 𝔸 (rename σ x) = rename σ (supp 𝔸 x)

theorem RenamingSets.isSupportOf_def' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] (A : Finset 𝔸) (x : X) : IsSupportOf A x ↔ ∀ ⦃f : Ren 𝔸⦄, (∀ a ∈ A, f a = a) → rename f x = x

theorem RenamingSets.supp_apply {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 X] [RenamingSet 𝔸 Y] [Infinite 𝔸] [DecidableEq 𝔸] {A : Finset 𝔸} {f : X → Y} (hf : IsSupportOfF A f) (x : X) : supp 𝔸 (f x) ⊆ A ∪ supp 𝔸 x

theorem RenamingSets.isSupportOf_rename {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq 𝔸] (σ : Ren 𝔸) {A : Finset 𝔸} {x : X} (hx : IsSupportOf A x) : IsSupportOf (rename σ A) (rename σ x)

theorem RenamingSets.isSupported_rename {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (σ : Ren 𝔸) {x : X} (hx : IsSupported 𝔸 x) : IsSupported 𝔸 (rename σ x)