Grace/Cumulus/Cardinal/Permutations.g17

Imports

Declarations

permutations def
inversions def
permutations.mem_iff theorem derivation
permutations.finite theorem derivation
inversions.finite theorem derivation
inversions.empty theorem derivation
permutations.empty theorem derivation
Source

1-- Finite sets of permutations and their inversion sets (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.Permutations8import FiniteSubsets9import Enumeration10import Product1112def permutations (I : Set) : Set := {p ∈ 𝒫(I × I) | BijectiveBetween(p, I, I)}1314def inversions (I p : Set) : Set :=15  {q ∈ I × I | ∃ i ∈ I, ∃ j ∈ I, q = (i, j) ∧ i ∈ j ∧ p(j) ∈ p(i)}1617theorem permutations.mem_iff (I p : Set)18  shows p ∈ permutations(I) ↔ BijectiveBetween(p, I, I)19proof20  constructor21  . intro member22    simp23  . intro bijective24    have injective := Bijective.injective with bijective25    have function := Injective.function with injective26    have relation := FunctionBetween.relation with function27    unfold RelationBetween at relation28    have bound := powerset.membership_iff.backward with relation29    simp3031theorem permutations.finite (I : Set)32  requires finite : Finite(I)33  shows Finite(permutations(I))34proof35  have product := Finite.product with finite, finite36  have powers := Finite.powerset with product37  have bounded : permutations(I) ⊆ 𝒫(I × I) by simp [Subset, permutations]38  exact Finite.subset with powers, bounded3940theorem inversions.finite (I p : Set)41  requires finite : Finite(I)42  shows Finite(inversions(I, p))43proof44  have product := Finite.product with finite, finite45  have bounded : inversions(I, p) ⊆ I × I by simp [Subset, inversions]46  exact Finite.subset with product, bounded4748theorem inversions.empty (p : Set)49  shows inversions(∅, p) = ∅50proof51  ext y52  simp [inversions, set.empty]5354theorem permutations.empty55  shows permutations(∅) = {∅}56proof57  have emptyFunction : ∅ : ∅ → ∅ by exact FunctionBetween.empty at ∅58  have emptyBijective : BijectiveBetween(∅, ∅, ∅)59    constructor60    . unfold InjectiveBetween61      refine ⟨emptyFunction, ?_⟩62      intros u impossible63      exfalso64      exact set.empty with impossible65    . unfold SurjectiveBetween66      refine ⟨emptyFunction, ?_⟩67      intros u impossible68      exfalso69      exact set.empty with impossible70  ext p71  constructor72  . intro member73    have bijective := permutations.mem_iff.forward with member74    have injective := Bijective.injective with bijective75    have function := Injective.function with injective76    have relation := FunctionBetween.relation with function77    have equal : p = ∅78      ext q79      constructor80      . intro hq81        unfold RelationBetween at relation82        have pair := relation with q, hq83        obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with pair84        exfalso85        exact set.empty with hi86      . intro impossible87        exfalso88        exact set.empty with impossible89    rw equal90    simp91  . intro member92    have equal := singleton.membership.forward with member93    rw equal94    exact permutations.mem_iff.backward with emptyBijective95