Natural Numbers

This file formalizes definitions and results about permutations and supports for natural numbers.

Permutations

instance NominalSets.Nat.instPermActionNat {𝔸 : Type u_1} : PermAction 𝔸 ℕ

Equations

• NominalSets.Nat.instPermActionNat = default

@[simp]

theorem NominalSets.Nat.perm_rec {𝔸 : Type u_1} {X : Type u_2} [PermAction 𝔸 X] (π : Perm 𝔸) (z : X) (s : ℕ → X → X) (n : ℕ) : perm π (Nat.rec z s n) = Nat.rec (perm π z) (perm π s) n

Supports

theorem NominalSets.Nat.isSupportedF_rec {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (z : X → Y) (hz : IsSupportedF 𝔸 z) (s : X → ℕ → Y → Y) (hs : IsSupportedF 𝔸 fun (x : X × ℕ × Y) => match x with | (x, y, z) => s x y z) (f : X → ℕ) (hf : IsSupportedF 𝔸 f) : IsSupportedF 𝔸 fun (x : X) => Nat.rec (z x) (s x) (f x)

Equivariance

theorem NominalSets.Nat.equivariant_rec {𝔸 : Type u_1} {X : Type u_2} {Y : Type u_3} [PermAction 𝔸 X] [PermAction 𝔸 Y] (z : X → Y) (hz : Equivariant 𝔸 z) (s : X → ℕ → Y → Y) (hs : Equivariant 𝔸 fun (x : X × ℕ × Y) => match x with | (x, y, z) => s x y z) (f : X → ℕ) (hf : Equivariant 𝔸 f) : Equivariant 𝔸 fun (x : X) => Nat.rec (z x) (s x) (f x)