Permutations

This file provides lemmas related to finite permutations.

@[simp]

theorem NominalSets.Perm.coe_mk {𝔸 : Type u_1} (π π' : 𝔸 → 𝔸) (hπ₁ : ∀ (a : 𝔸), π (π' a) = a) (hπ₂ : ∀ (a : 𝔸), π' (π a) = a) (hπ₃ : ∃ (A : Finset 𝔸), ∀ a ∉ A, π a = a) (x : 𝔸) : { toFun := π, invFun := π', right_inverse' := hπ₁, left_inverse' := hπ₂, has_supp' := hπ₃ } x = π x

theorem NominalSets.Perm.ext {𝔸 : Type u_1} {π₁ π₂ : Perm 𝔸} (h : ∀ (a : 𝔸), π₁ a = π₂ a) : π₁ = π₂

theorem NominalSets.Perm.ext_iff {𝔸 : Type u_1} {π₁ π₂ : Perm 𝔸} : π₁ = π₂ ↔ ∀ (a : 𝔸), π₁ a = π₂ a

@[simp]

theorem NominalSets.Perm.coe_injective {𝔸 : Type u_1} (π : Perm 𝔸) : Function.Injective ⇑π

@[simp]

theorem NominalSets.Perm.coe_inj {𝔸 : Type u_1} (π : Perm 𝔸) (a b : 𝔸) : π a = π b ↔ a = b

@[simp]

theorem NominalSets.Perm.inv_injective {𝔸 : Type u_1} : Function.Injective fun (x : Perm 𝔸) => x⁻¹

@[simp]

theorem NominalSets.Perm.inv_inj {𝔸 : Type u_1} {π₁ π₂ : Perm 𝔸} : π₁⁻¹ = π₂⁻¹ ↔ π₁ = π₂

@[simp]

theorem NominalSets.Perm.eta {𝔸 : Type u_1} {π₁ π₂ : Perm 𝔸} : ⇑π₁ = ⇑π₂ ↔ π₁ = π₂

instance NominalSets.Perm.instGroup {𝔸 : Type u_1} : Group (Perm 𝔸)

Equations

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

@[simp]

theorem NominalSets.Perm.inv_one {𝔸 : Type u_1} : 1⁻¹ = 1

@[simp]

theorem NominalSets.Perm.mul_assoc {𝔸 : Type u_1} (π₁ π₂ π₃ : Perm 𝔸) : π₁ * (π₂ * π₃) = π₁ * π₂ * π₃

@[simp]

theorem NominalSets.Perm.swap_swap {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) : swap a b * swap a b = 1

@[simp]

theorem NominalSets.Perm.swap_swap_l {𝔸 : Type u_1} [DecidableEq 𝔸] (π : Perm 𝔸) (a b : 𝔸) : π * swap a b * swap a b = π

theorem NominalSets.Perm.swap_comm {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) : swap a b = swap b a

@[simp]

theorem NominalSets.Perm.inv_swap {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) : (swap a b)⁻¹ = swap a b

@[simp]

theorem NominalSets.Perm.swap_eq {𝔸 : Type u_1} [DecidableEq 𝔸] (a : 𝔸) : swap a a = 1

theorem NominalSets.Perm.swap_mul {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) (π : Perm 𝔸) : swap a b * π = π * swap (π⁻¹ a) (π⁻¹ b)

theorem NominalSets.Perm.mul_swap {𝔸 : Type u_1} [DecidableEq 𝔸] (a b : 𝔸) (π : Perm 𝔸) : π * swap a b = swap (π a) (π b) * π

@[simp]

theorem NominalSets.Perm.seq_append {𝔸 : Type u_1} [DecidableEq 𝔸] (xs ys : List (𝔸 × 𝔸)) : seq (xs ++ ys) = seq xs * seq ys

theorem NominalSets.Perm.exists_seq {𝔸 : Type u_1} [DecidableEq 𝔸] (π : Perm 𝔸) : ∃ (xs : List (𝔸 × 𝔸)), π = seq xs

instance NominalSets.Perm.instCountable {𝔸 : Type u_1} [Countable 𝔸] : Countable (Perm 𝔸)