Documentation

RenamingSets.Support.Basic

IsSupportOf #

source
theorem RenamingSets.isSupportOf_def {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (A : Finset 𝔸) (x : X) :
IsSupportOf A x ↔ ∀ ⦃f g : Ren 𝔸⦄, (∀ a ∈ A, f a = g a) → rename f x = rename g x
source
theorem RenamingSets.isSupportOf_inter {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq 𝔸] {A B : Finset 𝔸} {x : X} (hA : IsSupportOf A x) (hB : IsSupportOf B x) :
IsSupportOf (A ∩ B) x
source
theorem RenamingSets.isSupportOf_mono {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (x : X) :
Monotone fun (x_1 : Finset 𝔸) => IsSupportOf x_1 x
source
theorem RenamingSets.isSupportOf_union_left {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq 𝔸] {A B : Finset 𝔸} {x : X} :
IsSupportOf A x → IsSupportOf (A ∪ B) x
source
theorem RenamingSets.isSupportOf_union_right {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DecidableEq 𝔸] {A B : Finset 𝔸} {x : X} :
IsSupportOf B x → IsSupportOf (A ∪ B) x
source
@[simp]
theorem RenamingSets.isSupportOf_discrete {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DiscreteRenameAction 𝔸 X] (A : Finset 𝔸) (x : X) :
IsSupportOf A x
source
@[simp]
theorem RenamingSets.isSupportOf_atom {𝔸 : Type u_1} [Infinite 𝔸] (A : Finset 𝔸) (a : 𝔸) :
IsSupportOf A a ↔ a ∈ A

IsSupportOfF #

source
theorem RenamingSets.isSupportOfF_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (A : Finset 𝔸) (f : X → Y) :
IsSupportOfF A f ↔ ∀ ⦃σ : Ren 𝔸⦄, (∀ a ∈ A, σ a = a) → ∀ (x : X), rename σ (f x) = f (rename σ x)
source
@[simp]
theorem RenamingSets.isSupportOfF_mono {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : X → Y) :
Monotone fun (x : Finset 𝔸) => IsSupportOfF x f
source
@[simp]
theorem RenamingSets.isSupportOfF_union_left {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [DecidableEq 𝔸] {A B : Finset 𝔸} (f : X → Y) (hf : IsSupportOfF A f) :
IsSupportOfF (A ∪ B) f
source
@[simp]
theorem RenamingSets.isSupportOfF_union_right {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [DecidableEq 𝔸] {A B : Finset 𝔸} (f : X → Y) (hf : IsSupportOfF B f) :
IsSupportOfF (A ∪ B) f
source
@[simp]
theorem RenamingSets.isSupportOfF_id {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (A : Finset 𝔸) :
IsSupportOfF A id
source
@[simp]
theorem RenamingSets.isSupportOfF_id' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (A : Finset 𝔸) :
IsSupportOfF A fun (x : X) => x
source
@[simp]
theorem RenamingSets.isSupportOfF_comp {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] (A : Finset 𝔸) {f : Y → Z} (hf : IsSupportOfF A f) {g : X → Y} (hg : IsSupportOfF A g) :
IsSupportOfF A (f ∘ g)
source
@[simp]
theorem RenamingSets.isSupportOfF_comp' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] (A : Finset 𝔸) {f : Y → Z} (hf : IsSupportOfF A f) {g : X → Y} (hg : IsSupportOfF A g) :
IsSupportOfF A fun (x : X) => f (g x)

IsSupported #

source
theorem RenamingSets.isSupported_def {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] (x : X) :
IsSupported 𝔸 x ↔ ∃ (A : Finset 𝔸), IsSupportOf A x
source
@[simp]
theorem RenamingSets.isSupported_discrete {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [DiscreteRenameAction 𝔸 X] (x : X) :
IsSupported 𝔸 x
source
@[simp]
theorem RenamingSets.isSupported_atom {𝔸 : Type u_1} (a : 𝔸) :
IsSupported 𝔸 a

IsSupportedF #

source
theorem RenamingSets.isSupportedF_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : X → Y) :
IsSupportedF 𝔸 f ↔ ∃ (A : Finset 𝔸), IsSupportOfF A f
source
noncomputable def RenamingSets.IsSupportedF.choose {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f : X → Y} (hf : IsSupportedF 𝔸 f) :
Finset 𝔸

Assuming IsSupportedF 𝔸 f, we can obtain some A : Finset 𝔸 such that IsSupportOfF A f.

Equations
Instances For
    source
    theorem RenamingSets.IsSupportedF.choose_spec {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f : X → Y} (hf : IsSupportedF 𝔸 f) :
    IsSupportOfF hf.choose f
    source
    @[simp]
    theorem RenamingSets.isSupportedF_id {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :
    IsSupportedF 𝔸 id
    source
    @[simp]
    theorem RenamingSets.isSupportedF_id' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :
    IsSupportedF 𝔸 fun (x : X) => x
    source
    @[simp]
    theorem RenamingSets.isSupportedF_comp {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : Y → Z} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) :
    IsSupportedF 𝔸 (f ∘ g)
    source
    @[simp]
    theorem RenamingSets.isSupportedF_comp' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : Y → Z} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) :
    IsSupportedF 𝔸 fun (x : X) => f (g x)
    source
    @[simp]
    theorem RenamingSets.isSupportedF_const {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenamingSet 𝔸 Y] (y : Y) :
    IsSupportedF 𝔸 fun (x : X) => y

    Equivariant #

    source
    theorem RenamingSets.equivariant_def {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] (f : X → Y) :
    Equivariant 𝔸 f ↔ IsSupportOfF ∅ f
    source
    @[simp]
    theorem RenamingSets.equivariant_id {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :
    Equivariant 𝔸 id
    source
    @[simp]
    theorem RenamingSets.equivariant_id' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] :
    Equivariant 𝔸 fun (x : X) => x
    source
    @[simp]
    theorem RenamingSets.equivariant_comp {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : Y → Z} (hf : Equivariant 𝔸 f) {g : X → Y} (hg : Equivariant 𝔸 g) :
    Equivariant 𝔸 (f ∘ g)
    source
    @[simp]
    theorem RenamingSets.equivariant_comp' {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] [RenameAction 𝔸 Z] {f : Y → Z} (hf : Equivariant 𝔸 f) {g : X → Y} (hg : Equivariant 𝔸 g) :
    Equivariant 𝔸 fun (x : X) => f (g x)
    source
    theorem RenamingSets.isSupportedF_of_equivariant {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [RenameAction 𝔸 X] [RenameAction 𝔸 Y] {f : X → Y} (hf : Equivariant 𝔸 f) :
    IsSupportedF 𝔸 f

    RenamingSet #

    source
    instance RenamingSets.instRenamingSet {𝔸 : Type u_1} {X : Type u_2} :
    RenamingSet 𝔸 X
    source
    instance RenamingSets.instRenamingSet_1 {𝔸 : Type u_1} :
    RenamingSet 𝔸 𝔸

    supp #

    source
    theorem RenamingSets.mem_supp {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] (a : 𝔸) (x : X) :
    a ∈ supp 𝔸 x ↔ ∀ (A : Finset 𝔸), IsSupportOf A x → a ∈ A
    source
    theorem RenamingSets.supp_min {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] {A : Finset 𝔸} {x : X} (h : IsSupportOf A x) :
    supp 𝔸 x ⊆ A
    source
    @[simp]
    theorem RenamingSets.isSupportOf_supp {X : Type u_2} (𝔸 : Type u_5) [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] (x : X) :
    IsSupportOf (supp 𝔸 x) x
    source
    theorem RenamingSets.rename_congr {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] {f g : Ren 𝔸} (x : X) (h : ∀ a ∈ supp 𝔸 x, f a = g a) :
    rename f x = rename g x
    source
    theorem RenamingSets.rename_congr' {𝔸 : Type u_1} {X : Type u_2} [RenameAction 𝔸 X] [RenamingSet 𝔸 X] [Infinite 𝔸] {f : Ren 𝔸} (x : X) (h : ∀ a ∈ supp 𝔸 x, f a = a) :
    rename f x = x
    source
    @[simp]
    theorem RenamingSets.supp_atom {𝔸 : Type u_1} [Infinite 𝔸] (a : 𝔸) :
    supp 𝔸 a = {a}