instance NominalSets.Prop.instPermActionProp {𝔸 : Type u_1} : PermAction 𝔸 Prop

Equations

• NominalSets.Prop.instPermActionProp = default

@[simp]

theorem NominalSets.Prop.isSupportedF_ite {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] {p : X → Prop} (hp : IsSupportedF 𝔸 p) [DecidablePred p] {f : X → Y} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => if p x then f x else g x

theorem NominalSets.Prop.isSupportedF_eq {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] [DiscretePermAction 𝔸 Y] {f : X → Y} (hf : IsSupportedF 𝔸 f) {g : X → Y} (hg : IsSupportedF 𝔸 g) : IsSupportedF 𝔸 fun (x : X) => f x = g x