Grace/Cumulus/Combinatorics/Permutations.g17

Open in Workbench Download source

Imports

Injections

Declarations

• permutations.eq_bijections theorem derivation
• permutations.of_bijective theorem derivation
• permutations.bijective theorem derivation
• permutations.function theorem derivation
• permutations.count theorem derivation
• permutations.natural_count theorem derivation
• permutations.identity theorem derivation
• permutations.nonempty theorem derivation
• permutations.compose theorem derivation
• permutations.converse theorem derivation
• permutations.transposition theorem derivation
• permutations.apply_closed theorem derivation
• permutations.apply_cancel theorem derivation
• permutations.apply_surjective theorem derivation
• permutations.image_full theorem derivation
• permutations.inverse_apply theorem derivation
• permutations.apply_inverse theorem derivation
• permutations.compose_identity_left theorem derivation
• permutations.compose_identity_right theorem derivation
• permutations.compose_associative theorem derivation
• permutations.of_injective theorem derivation
• permutations.of_surjective theorem derivation
• permutations.eq_injections theorem derivation
• permutations.singleton theorem derivation
• permutations.two_count theorem derivation
• permutations.three_count theorem derivation

Source

1-- Permutations of a finite set: the bijections of a set onto itself form2-- a set of size n!, closed under composition and inversion and containing3-- the identity and every transposition4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Combinatorics.Permutations10import Injections1112theorem permutations.eq_bijections (I : Set)13  shows permutations(I) = bijections(I, I)14proof15  ext p16  constructor17  . intro member18    exact bijections.of_bijective with (permutations.mem_iff.forward with member)19  . intro member20    exact permutations.mem_iff.backward with (bijections.bijective with member)2122theorem permutations.of_bijective (I p : Set)23  requires bijective : BijectiveBetween(p, I, I)24  shows p ∈ permutations(I)25proof26  exact permutations.mem_iff.backward with bijective2728theorem permutations.bijective (I p : Set)29  requires member : p ∈ permutations(I)30  shows BijectiveBetween(p, I, I)31proof32  exact permutations.mem_iff.forward with member3334theorem permutations.function (I p : Set)35  requires member : p ∈ permutations(I)36  shows p : I → I37proof38  have bijective := permutations.bijective with member39  exact Injective.function with (Bijective.injective with bijective)4041-- A finite set with n elements has n! permutations.42theorem permutations.count (I : Set)43  requires finite : Finite(I)44  shows cardinality(permutations(I)) = cardinality(I)!45proof46  rw permutations.eq_bijections47  exact bijections.count_self with finite4849theorem permutations.natural_count (n : Nat)50  shows cardinality(permutations(n)) = n!51proof52  have count := permutations.count with (Finite.natural at n)53  rw [count, cardinality.natural]54  rfl5556theorem permutations.identity (I : Set)57  shows identity(I) ∈ permutations(I)58proof59  exact permutations.of_bijective with (identity.bijective at I)6061theorem permutations.nonempty (I : Set)62  shows Nonempty(permutations(I))63proof64  exact ⟨identity(I), permutations.identity at I⟩6566theorem permutations.compose (I p q : Set)67  requires hp : p ∈ permutations(I)68  requires hq : q ∈ permutations(I)69  shows compose(q, p, I, I, I) ∈ permutations(I)70proof71  have pBijective := permutations.bijective with hp72  have qBijective := permutations.bijective with hq73  have composed := compose.bijective at q, p, I, I, I with74    pBijective, qBijective75  exact permutations.of_bijective with composed7677theorem permutations.converse (I p : Set)78  requires hp : p ∈ permutations(I)79  shows converse(p, I, I) ∈ permutations(I)80proof81  have bijective := permutations.bijective with hp82  exact permutations.of_bijective with (converse.bijective with bijective)8384theorem permutations.transposition (I a b : Set)85  requires ha : a ∈ I86  requires hb : b ∈ I87  shows transposition(I, a, b) ∈ permutations(I)88proof89  have bijective := transposition.bijective at I, a, b with ha, hb90  exact permutations.of_bijective with bijective9192theorem permutations.apply_closed (I p x : Set)93  requires hp : p ∈ permutations(I)94  requires hx : x ∈ I95  shows p(x) ∈ I96proof97  exact FunctionBetween.apply_closed with (permutations.function with hp), hx9899theorem permutations.apply_cancel (I p x y : Set)100  requires hp : p ∈ permutations(I)101  requires hx : x ∈ I102  requires hy : y ∈ I103  requires same : p(x) = p(y)104  shows x = y105proof106  have injective := Bijective.injective with (permutations.bijective with hp)107  exact Injective.apply_cancel with injective, hx, hy, same108109theorem permutations.apply_surjective (I p y : Set)110  requires hp : p ∈ permutations(I)111  requires hy : y ∈ I112  shows ∃ x ∈ I, p(x) = y113proof114  have bijective := permutations.bijective with hp115  have surjective := Bijective.surjective with bijective116  have function := permutations.function with hp117  obtain ⟨x, hx, related⟩ := surjective.right with y, hy118  refine ⟨x, hx, ?_⟩119  exact FunctionBetween.apply_value with function, hx, related120121theorem permutations.image_full (I p : Set)122  requires hp : p ∈ permutations(I)123  shows functionImage(p, I, I) = I124proof125  have bijective := permutations.bijective with hp126  exact Surjective.image_full with (Bijective.surjective with bijective)127128theorem permutations.inverse_apply (I p x : Set)129  requires hp : p ∈ permutations(I)130  requires hx : x ∈ I131  shows converse(p, I, I)(p(x)) = x132proof133  exact Bijective.inverse_apply with (permutations.bijective with hp), hx134135theorem permutations.apply_inverse (I p y : Set)136  requires hp : p ∈ permutations(I)137  requires hy : y ∈ I138  shows p(converse(p, I, I)(y)) = y139proof140  exact Bijective.apply_inverse with (permutations.bijective with hp), hy141142theorem permutations.compose_identity_left (I p : Set)143  requires hp : p ∈ permutations(I)144  shows compose(identity(I), p, I, I, I) = p145proof146  exact compose.identity_left with (permutations.function with hp)147148theorem permutations.compose_identity_right (I p : Set)149  requires hp : p ∈ permutations(I)150  shows compose(p, identity(I), I, I, I) = p151proof152  exact compose.identity_right with (permutations.function with hp)153154theorem permutations.compose_associative (I p q r : Set)155  requires hp : p ∈ permutations(I)156  requires hq : q ∈ permutations(I)157  requires hr : r ∈ permutations(I)158  shows159    compose(r, compose(q, p, I, I, I), I, I, I) = compose(compose(r, q, I, I, I), p, I, I, I)160proof161  have pFunction := permutations.function with hp162  have qFunction := permutations.function with hq163  have rFunction := permutations.function with hr164  exact compose.associative at r, q, p, I, I, I, I with pFunction, qFunction, rFunction165166-- On a finite set an injective self-map is already a permutation.167theorem permutations.of_injective (I p : Set)168  requires finite : Finite(I)169  requires injective : InjectiveBetween(p, I, I)170  shows p ∈ permutations(I)171proof172  exact permutations.of_bijective with (Finite.self_injective_bijective with injective, finite)173174theorem permutations.of_surjective (I p : Set)175  requires finite : Finite(I)176  requires surjective : SurjectiveBetween(p, I, I)177  shows p ∈ permutations(I)178proof179  exact permutations.of_bijective with (Finite.self_surjective_bijective with surjective, finite)180181theorem permutations.eq_injections (I : Set)182  requires finite : Finite(I)183  shows permutations(I) = injections(I, I)184proof185  have same : cardinality(I) = cardinality(I) by rfl186  rw permutations.eq_bijections187  exact bijections.eq_injections with finite, same188189-- A singleton has only the identity permutation.190theorem permutations.singleton (x : Set)191  shows permutations({x}) = {identity({x})}192proof193  have finite := Finite.singleton at x194  have count := permutations.count with finite195  rw [cardinality.singleton, factorial.one] at count196  have finitePerms := permutations.finite with finite197  have iff := cardinality.one_iff with finitePerms198  obtain ⟨y, shape⟩ := iff.forward with count199  have member := permutations.identity at {x}200  rw shape at member201  have equal := singleton.membership.forward with member202  rw [shape, equal]203  rfl204205theorem permutations.two_count206  shows cardinality(permutations(2)) = 2207proof208  have count := permutations.natural_count at 2209  rw count210  compute211212theorem permutations.three_count213  shows cardinality(permutations(3)) = 6214proof215  have count := permutations.natural_count at 3216  rw count217  compute218