Grace/Cumulus/Combinatorics/Injections.g17

Open in Workbench Download source

Imports

Functions

Declarations

Source

1-- Counting injections: the falling factorial n · (n − 1) ⋯ (n − m + 1)2-- counts the injections from an m-element set into an n-element set, and3-- the bijections between two n-element sets number n!4-- 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.Injections10import Functions1112def injections (A B : Set) : Set :=13  { f ∈ functionSpace(A, B) | InjectiveBetween(f, A, B) }1415theorem injections.of_injective (f A B : Set)16  requires injective : InjectiveBetween(f, A, B)17  shows f ∈ injections(A, B)18proof19  have function := Injective.function with injective20  have inSpace := functionSpace.mem_iff.backward with function21  exact injections.membership.backward with ⟨inSpace, injective⟩2223theorem injections.injective (f A B : Set)24  requires member : f ∈ injections(A, B)25  shows InjectiveBetween(f, A, B)26proof27  have parts := injections.membership.forward with member28  exact parts.right2930theorem injections.function (f A B : Set)31  requires member : f ∈ injections(A, B)32  shows f : A → B33proof34  exact Injective.function with (injections.injective with member)3536theorem injections.subset (A B : Set)37  shows injections(A, B) ⊆ functionSpace(A, B)38proof39  intros f hf40  have parts := injections.membership.forward with hf41  exact parts.left4243theorem injections.finite (A B : Set)44  requires finiteA : Finite(A)45  requires finiteB : Finite(B)46  shows Finite(injections(A, B))47proof48  have space := functionSpace.finite with finiteA, finiteB49  exact Finite.subset with space, (injections.subset at A, B)5051theorem injections.empty_domain (B : Set)52  shows injections(∅, B) = {∅}53proof54  have emptyFunction := FunctionBetween.empty at B55  have emptyInjective : InjectiveBetween(∅, ∅, B)56    unfold InjectiveBetween57    refine ⟨emptyFunction, ?_⟩58    intros u impossible59    exfalso60    exact set.empty with impossible61  ext f62  constructor63  . intro member64    have parts := injections.membership.forward with member65    have inSpace := parts.left66    rw functionSpace.empty_domain at inSpace67    exact inSpace68  . intro member69    have equal := singleton.membership.forward with member70    rw equal71    exact injections.of_injective with emptyInjective7273theorem injections.empty_domain_count (B : Set)74  shows cardinality(injections(∅, B)) = 175proof76  rw injections.empty_domain77  exact cardinality.singleton at ∅7879theorem injections.empty_codomain (A : Set)80  requires nonempty : Nonempty(A)81  shows injections(A, ∅) = ∅82proof83  have empty := functionSpace.empty_codomain with nonempty84  have subset := injections.subset at A, ∅85  rw empty at subset86  exact Subset.empty_iff.forward with subset8788-- The falling factorial n · (n − 1) ⋯ (n − m + 1), zero once m exceeds n.89def fallingFactorial (n m : Nat) → Nat90  | n, zero => 191  | n, succ(m) => mul(fallingFactorial(n, m), sub(n, m))92  descends m9394theorem fallingFactorial.zero (n : Nat)95  shows fallingFactorial(n, 0) = 196proof97  simp [fallingFactorial]9899theorem fallingFactorial.succ (n m : Nat)100  shows fallingFactorial(n, m + 1) = fallingFactorial(n, m) * (n - m)101proof102  have hm : m + 1 = succ(m) := add.right_one with *103  rw hm104  simp [fallingFactorial]105106theorem fallingFactorial.natural (n m : Nat)107  shows Nat(fallingFactorial(n, m))108proof109  induction m110  | zero =>111    rw fallingFactorial.zero112    typecheck113  | j + 1 using ih =>114    rw fallingFactorial.succ115    have subNat := sub.closed at n, j116    typecheck117118theorem fallingFactorial.one (n : Nat)119  shows fallingFactorial(n, 1) = n120proof121  have one : 0 + 1 = 1 by compute122  rw ← one123  rw [fallingFactorial.succ, fallingFactorial.zero, sub.zero_right]124  ring125126theorem fallingFactorial.zero_left (m : Nat)127  shows fallingFactorial(0, m + 1) = 0128proof129  rw [fallingFactorial.succ, sub.zero_left]130  have natural := fallingFactorial.natural at 0, m131  ring132133-- The recursion on the first argument, free of subtraction.134theorem fallingFactorial.succ_succ (n m : Nat)135  shows fallingFactorial(n + 1, m + 1) = (n + 1) * fallingFactorial(n, m)136proof137  induction m138  | zero =>139    have one : 0 + 1 = 1 by compute140    rw [one, fallingFactorial.one, fallingFactorial.zero]141    ring142  | j + 1 using ih =>143    rw [fallingFactorial.succ, ih]144    have hn : n + 1 = succ(n) := add.right_one with *145    have hj : j + 1 = succ(j) := add.right_one with *146    rw [hn, hj, sub.succ_succ, ← hj]147    rw fallingFactorial.succ148    have natural := fallingFactorial.natural at n, j149    have subNat := sub.closed at n, j150    ring151152theorem fallingFactorial.self (n : Nat)153  shows fallingFactorial(n, n) = n!154proof155  induction n156  | zero => compute157  | k + 1 using ih =>158    rw [fallingFactorial.succ_succ, ih, factorial.succ]159    rfl160161theorem fallingFactorial.self_vanishes (n : Nat)162  shows fallingFactorial(n, n + 1) = 0163proof164  rw fallingFactorial.succ165  have shape : 0 + n = n by ring166  have difference : n - n = 0167    have step := sub.add_right at 0, n168    rw shape at step169    exact step170  rw difference171  have natural := fallingFactorial.natural at n, n172  ring173174theorem fallingFactorial.beyond (n d : Nat)175  shows fallingFactorial(n, n + 1 + d) = 0176proof177  induction d178  | zero =>179    have shape : n + 1 + 0 = n + 1 by ring180    rw shape181    exact fallingFactorial.self_vanishes at n182  | j + 1 using ih =>183    have shape : n + 1 + (j + 1) = (n + 1 + j) + 1 by ring184    rw [shape, fallingFactorial.succ, ih]185    have subNat := sub.closed at n, n + 1 + j186    ring187188theorem fallingFactorial.of_Less (n m : Nat)189  requires below : n < m190  shows fallingFactorial(n, m) = 0191proof192  obtain ⟨d, dNat, shape⟩ := below193  have form : m = n + 1 + d194    rw ← shape195    ring196  rw form197  exact fallingFactorial.beyond at n, d198199theorem fallingFactorial.mul_factorial (k : Nat)200  shows ∀ d, Nat(d) → fallingFactorial(k + d, k) * d! = (k + d)!201proof202  induction k203  | zero =>204    intros d dNat205    have shape : 0 + d = d by ring206    rw [shape, fallingFactorial.zero]207    have closed := factorial.closed at d208    ring209  | j + 1 using ih =>210    intros d dNat211    have shape : j + 1 + d = (j + d) + 1 by ring212    rw [shape, fallingFactorial.succ_succ]213    have inner := ih with d, dNat214    rw factorial.succ215    have natural := fallingFactorial.natural at j + d, j216    have closedD := factorial.closed at d217    have closedTop := factorial.closed at j + d218    ring [inner]219220-- The falling factorial is the binomial coefficient times k!.221theorem fallingFactorial.choose (n k : Nat)222  requires le : k ≤ n223  shows fallingFactorial(n, k) = (n choose k) * k!224proof225  obtain ⟨d, dNat, shape⟩ := le226  have form : n = k + d227    rw ← shape228    rfl229  rw form230  have row := fallingFactorial.mul_factorial at k231  have first := row with d, dNat232  have commute : k + d = d + k by ring233  have chooseRow := choose.factorial at d234  have second := chooseRow with k, assumption235  rw ← commute at second236  have natural := fallingFactorial.natural at k + d, k237  have chooseNat := choose.natural at k + d, k238  have closedK := factorial.closed at k239  have closedD := factorial.closed at d240  have nonzero := factorial.nonzero at d241  have balanced : d! * fallingFactorial(k + d, k) = d! * (((k + d) choose k) * k!) by ring [first, second]242  exact mul.left_cancel_positive with nonzero, balanced243244-- Changing the codomain of an injection.245theorem Injective.widen (f A B C : Set)246  requires injective : InjectiveBetween(f, A, B)247  requires subset : B ⊆ C248  shows InjectiveBetween(f, A, C)249proof250  have function := Injective.function with injective251  have values : ∀ x ∈ A, f(x) ∈ C252    intros x hx253    exact subset with f(x), (FunctionBetween.apply_closed with function, hx)254  have widened := FunctionBetween.codomain_of_values with function, values255  apply Injective.of_pointwise with widened256  intros x hx y hy same257  exact Injective.apply_cancel with injective, hx, hy, same258259theorem Injective.avoid (g A B b : Set)260  requires injective : InjectiveBetween(g, A, B)261  requires absent : ¬b ∈ functionImage(g, A, B)262  shows InjectiveBetween(g, A, B ∖ {b})263proof264  have function := Injective.function with injective265  have values : ∀ x ∈ A, g(x) ∈ B ∖ {b}266    intros x hx267    apply difference.singleton_membership.backward268    constructor269    . exact FunctionBetween.apply_closed with function, hx270    . intro same271      apply absent272      rw ← same273      exact functionImage.value with function, hx274  have narrowed := FunctionBetween.codomain_of_values with function, values275  apply Injective.of_pointwise with narrowed276  intros x hx y hy same277  exact Injective.apply_cancel with injective, hx, hy, same278279-- Pairs of an injection on A and a point of B, split by whether the point280-- is already a value.281def freshPairs (A B : Set) : Set :=282  { p ∈ injections(A, B) × B | ∃ g ∈ injections(A, B), ∃ b ∈ B, p = (g, b) ∧ ¬b ∈ functionImage(g, A, B) }283284def coveredPairs (A B : Set) : Set :=285  { p ∈ injections(A, B) × B | ∃ g ∈ injections(A, B), ∃ b ∈ B, p = (g, b) ∧ b ∈ functionImage(g, A, B) }286287theorem freshPairs.pair (A B g b : Set)288  shows289    (g, b) ∈ freshPairs(A, B) ↔ g ∈ injections(A, B) ∧ b ∈ B ∧ ¬b ∈ functionImage(g, A, B)290proof291  constructor292  . intro member293    obtain ⟨bound, h, hh, c, hc, shape, absent⟩ := freshPairs.membership.forward with member294    have coordinates := orderedPair.injective with shape295    rw [coordinates.left, coordinates.right]296    exact ⟨hh, hc, absent⟩297  . intro parts298    obtain ⟨hg, hb, absent⟩ := parts299    apply freshPairs.membership.backward300    refine ⟨(product.pair with hg, hb), g, hg, b, hb, rfl, absent⟩301302theorem coveredPairs.pair (A B g b : Set)303  shows304    (g, b) ∈ coveredPairs(A, B) ↔ g ∈ injections(A, B) ∧ b ∈ B ∧ b ∈ functionImage(g, A, B)305proof306  constructor307  . intro member308    obtain ⟨bound, h, hh, c, hc, shape, covered⟩ := coveredPairs.membership.forward with member309    have coordinates := orderedPair.injective with shape310    rw [coordinates.left, coordinates.right]311    exact ⟨hh, hc, covered⟩312  . intro parts313    obtain ⟨hg, hb, covered⟩ := parts314    apply coveredPairs.membership.backward315    refine ⟨(product.pair with hg, hb), g, hg, b, hb, rfl, covered⟩316317theorem freshPairs.subset (A B : Set)318  shows freshPairs(A, B) ⊆ injections(A, B) × B319proof320  intros p hp321  have parts := freshPairs.membership.forward with hp322  exact parts.left323324theorem coveredPairs.subset (A B : Set)325  shows coveredPairs(A, B) ⊆ injections(A, B) × B326proof327  intros p hp328  have parts := coveredPairs.membership.forward with hp329  exact parts.left330331theorem freshPairs.disjoint (A B : Set)332  shows Disjoint(freshPairs(A, B), coveredPairs(A, B))333proof334  apply Disjoint.iff.backward335  intros p fresh covered336  obtain ⟨bound, g, hg, b, hb, shape, absent⟩ := freshPairs.membership.forward with fresh337  rw shape at covered338  have parts := coveredPairs.pair.forward with covered339  exact absent with parts.right.right340341theorem freshPairs.union (A B : Set)342  shows freshPairs(A, B) ∪ coveredPairs(A, B) = injections(A, B) × B343proof344  ext p345  constructor346  . intro hp347    have split := union2.membership.forward with hp348    cases split with fresh | covered349    . exact freshPairs.subset at A, B with p, fresh350    . exact coveredPairs.subset at A, B with p, covered351  . intro hp352    obtain ⟨bound, g, hg, b, hb, shape⟩ := product.membership.forward with hp353    rw shape354    have alternatives : b ∈ functionImage(g, A, B) ∨ ¬b ∈ functionImage(g, A, B) by tauto355    cases alternatives with covered | absent356    . apply union2.right357      exact coveredPairs.pair.backward with ⟨hg, hb, covered⟩358    . apply union2.left359      exact freshPairs.pair.backward with ⟨hg, hb, absent⟩360361theorem freshPairs.finite (A B : Set)362  requires finiteA : Finite(A)363  requires finiteB : Finite(B)364  shows Finite(freshPairs(A, B))365proof366  have product := Finite.product with (injections.finite with367    finiteA, finiteB), finiteB368  exact Finite.subset with product, (freshPairs.subset at A, B)369370theorem coveredPairs.finite (A B : Set)371  requires finiteA : Finite(A)372  requires finiteB : Finite(B)373  shows Finite(coveredPairs(A, B))374proof375  have product := Finite.product with (injections.finite with376    finiteA, finiteB), finiteB377  exact Finite.subset with product, (coveredPairs.subset at A, B)378379-- Splitting an injection on insert(a, A) into its restriction and its380-- value at a lands exactly on the fresh pairs.381theorem injections.restrict (f A B a : Set)382  requires member : f ∈ injections(insert(a, A), B)383  shows restrict(f, A) ∈ injections(A, B)384proof385  have injective := injections.injective with member386  have restricted := restrict.injective with387    injective, (insert.subset_self at A, a)388  exact injections.of_injective with restricted389390theorem injections.value_fresh (f A B a : Set)391  requires fresh : ¬a ∈ A392  requires member : f ∈ injections(insert(a, A), B)393  shows ¬f(a) ∈ functionImage(restrict(f, A), A, B)394proof395  intro covered396  have injective := injections.injective with member397  have function := injections.function with member398  have subset := insert.subset_self at A, a399  obtain ⟨inB, x, hx, shape⟩ := functionImage.membership.forward with covered400  have step := restrict.domain_apply with function, subset, hx401  rw step at shape402  have equal := Injective.apply_cancel with injective, (insert.self at a, A), (subset with x, hx), shape403  apply fresh404  rw equal405  exact hx406407theorem injections.adjoin (g A B a b : Set)408  requires fresh : ¬a ∈ A409  requires hg : g ∈ injections(A, B)410  requires hb : b ∈ B411  requires absent : ¬b ∈ functionImage(g, A, B)412  shows adjoinMap(g, a, b) ∈ injections(insert(a, A), B)413proof414  have injective := injections.injective with hg415  have narrowed := Injective.avoid with injective, absent416  have notIn : ¬b ∈ B ∖ {b} by simp [difference.membership, singleton.membership]417  have extended := adjoinMap.injective at g, A, B ∖ {b}, a, b with418    narrowed, fresh, notIn419  have restored := insert.restore with hb420  rw restored at extended421  exact injections.of_injective with extended422423theorem injections.split_image (A B a : Set)424  requires fresh : ¬a ∈ A425  shows426    functionImage(functionSplit(A, B, a), injections(insert(a, A), B), functionSpace(A, B) × B) = freshPairs(A, B)427proof428  have function := functionSplit.function at A, B, a429  ext p430  constructor431  . intro hp432    obtain ⟨bound, f, hf, shape⟩ := functionImage.membership.forward with hp433    have inSpace := injections.subset at insert(a, A), B with f, hf434    have value := functionSplit.value at A, B, a, f with inSpace435    rw [shape, value]436    apply freshPairs.pair.backward437    have restricted := injections.restrict with hf438    have inB := FunctionBetween.apply_closed with (injections.function with439      hf), (insert.self at a, A)440    have absent := injections.value_fresh with fresh, hf441    exact ⟨restricted, inB, absent⟩442  . intro hp443    obtain ⟨bound, g, hg, b, hb, shape, absent⟩ := freshPairs.membership.forward with hp444    have adjoined := injections.adjoin with fresh, hg, hb, absent445    have gSpace := injections.subset at A, B with g, hg446    have value := functionSplit.adjoin_value with fresh, gSpace, hb447    apply functionImage.membership.backward448    constructor449    . rw shape450      exact product.pair with gSpace, hb451    . witness adjoinMap(g, a, b)452      constructor453      . exact adjoined454      . rw [shape, value]455        rfl456457theorem injections.insert_equipotent (A B a : Set)458  requires fresh : ¬a ∈ A459  shows injections(insert(a, A), B) ≃ freshPairs(A, B)460proof461  have injective := functionSplit.injective at A, B, a462  have function := functionSplit.function at A, B, a463  have subset := injections.subset at insert(a, A), B464  have restricted := restrict.injective with injective, subset465  have equipotent := Equipotent.image with restricted466  have sameImage := functionImage.restrict with function, subset467  have image := injections.split_image at A, B, a with fresh468  rwa [sameImage, image] at equipotent469470-- The covered pairs are the pairs (g, x) of an injection and a point of471-- its domain, through (g, x) ↦ (g, g(x)).472defunique coveredPair (A B p : Set) (q ∈ injections(A, B) × B) :=473  ∃ g ∈ injections(A, B), ∃ x ∈ A, p = (g, x) ∧ q = (g, g(x))474requires pair : p ∈ injections(A, B) × A475proof476  obtain ⟨bound, g, hg, x, hx, shape⟩ := product.membership.forward with pair477  have function := injections.function with hg478  have value := FunctionBetween.apply_closed with function, hx479  have output := product.pair with hg, value480  refine ⟨(g, g(x)), output, g, hg, x, hx, shape, rfl⟩481uniqueness482  intros u hu first v hv second483  obtain ⟨g, hg, x, hx, shapeU, valueU⟩ := first484  obtain ⟨h, hh, y, hy, shapeV, valueV⟩ := second485  have equal : (g, x) = (h, y) by cc486  have coordinates := orderedPair.injective with equal487  cc488489defgraph coveredMap (A B : Set) (p ∈ injections(A, B) × A) : injections(A, B) × B := coveredPair(A, B, p)490proof491  have selected := coveredPair.selected with member492  exact selected.left493494theorem coveredMap.pair (A B g x : Set)495  requires hg : g ∈ injections(A, B)496  requires hx : x ∈ A497  shows coveredMap(A, B)((g, x)) = (g, g(x))498proof499  have pair := product.pair at g, x, injections(A, B), A with *500  have selected := coveredPair.selected with pair501  obtain ⟨h, hh, y, hy, shape, output⟩ := selected.right502  have coordinates := orderedPair.injective with shape503  have value := coveredMap.value with pair504  cc505506theorem coveredMap.injective (A B : Set)507  shows508    InjectiveBetween(coveredMap(A, B), injections(A, B) × A, injections(A, B) × B)509proof510  have function := coveredMap.function at A, B511  apply Injective.of_pointwise with function512  intros p hp q hq same513  obtain ⟨boundP, g, hg, x, hx, shapeP⟩ := product.membership.forward with hp514  obtain ⟨boundQ, h, hh, y, hy, shapeQ⟩ := product.membership.forward with hq515  have valueP := coveredMap.pair with hg, hx516  have valueQ := coveredMap.pair with hh, hy517  rw [shapeP, shapeQ, valueP, valueQ] at same518  have coordinates := orderedPair.injective with same519  have sameFunction := coordinates.left520  have sameValue := coordinates.right521  rw ← sameFunction at sameValue522  have injective := injections.injective with hg523  have sameInput := Injective.apply_cancel with injective, hx, hy, sameValue524  rw [shapeP, shapeQ, sameFunction, sameInput]525  rfl526527theorem coveredMap.image (A B : Set)528  shows529    functionImage(coveredMap(A, B), injections(A, B) × A, injections(A, B) × B) = coveredPairs(A, B)530proof531  have function := coveredMap.function at A, B532  ext q533  constructor534  . intro hq535    obtain ⟨bound, p, hp, shape⟩ := functionImage.membership.forward with hq536    obtain ⟨boundP, g, hg, x, hx, shapeP⟩ := product.membership.forward with hp537    have value := coveredMap.pair with hg, hx538    rw [shape, shapeP, value]539    apply coveredPairs.pair.backward540    have gFunction := injections.function with hg541    have inB := FunctionBetween.apply_closed with gFunction, hx542    have covered := functionImage.value with gFunction, hx543    exact ⟨hg, inB, covered⟩544  . intro hq545    obtain ⟨bound, g, hg, b, hb, shape, covered⟩ := coveredPairs.membership.forward with hq546    obtain ⟨inB, x, hx, valueShape⟩ := functionImage.membership.forward with covered547    have pair := product.pair at g, x, injections(A, B), A with hg, hx548    have value := coveredMap.pair with hg, hx549    apply functionImage.membership.backward550    constructor551    . exact bound552    . witness (g, x)553      constructor554      . exact pair555      . rw [shape, value, valueShape]556        rfl557558theorem coveredPairs.equipotent (A B : Set)559  shows injections(A, B) × A ≃ coveredPairs(A, B)560proof561  have equipotent := Equipotent.image with (coveredMap.injective at A, B)562  rw coveredMap.image at equipotent563  exact equipotent564565-- Truncated subtraction distributes over a product.566theorem sub.self_add (a d : Nat)567  shows a - (a + d) = 0568proof569  induction d570  | zero =>571    have shape : a + 0 = a by ring572    rw shape573    have step := sub.add_right at 0, a574    have zero : 0 + a = a by ring575    rw zero at step576    exact step577  | j + 1 using ih =>578    have shape : a + (j + 1) = succ(a + j) by ring579    rw [shape, sub.succ_right, ih]580    exact predecessor.zero581582theorem sub.vanishes_of_le (a b : Nat)583  requires le : a ≤ b584  shows a - b = 0585proof586  obtain ⟨d, dNat, shape⟩ := le587  rw ← shape588  exact sub.self_add at a, d589590theorem mul.sub_distributes (a n m : Nat)591  shows a * (n - m) = a * n - a * m592proof593  have alternatives := LessEqual.total at m, n594  cases alternatives with le | ge595  . obtain ⟨d, dNat, shape⟩ := le596    rw ← shape597    have left : m + d - m = d598      have commute : m + d = d + m by ring599      rw commute600      exact sub.add_right at d, m601    have right : a * (m + d) - a * m = a * d602      have expand : a * (m + d) = a * d + a * m by ring603      rw expand604      exact sub.add_right at a * d, a * m605    rw [left, right]606    rfl607  . have zero := sub.vanishes_of_le with ge608    have bound := LessEqual.mul_left at n, m, a with ge609    have productZero := sub.vanishes_of_le with bound610    rw [zero, productZero]611    ring612613-- The count of injections grows by the factor n − m when the domain grows614-- by a point.615theorem injections.insert_count (A B a : Set) (m n : Nat)616  requires fresh : ¬a ∈ A617  requires countedA : HasCardinality(A, m)618  requires countedB : HasCardinality(B, n)619  requires counted : HasCardinality(injections(A, B), fallingFactorial(n, m))620  shows HasCardinality(injections(insert(a, A), B), fallingFactorial(n, m + 1))621proof622  have finiteA := Finite.from_cardinality with countedA623  have finiteB := Finite.from_cardinality with countedB624  have finiteInj := Finite.from_cardinality with counted625  have sizeA := cardinality.eq_of_has with countedA626  have sizeB := cardinality.eq_of_has with countedB627  have sizeInj := cardinality.eq_of_has with counted628  have finiteFresh := freshPairs.finite with finiteA, finiteB629  have finiteCovered := coveredPairs.finite with finiteA, finiteB630  have split := cardinality.union_disjoint with631    finiteFresh, finiteCovered, (freshPairs.disjoint at A, B)632  rw freshPairs.union at split633  have productB := cardinality.product_count with finiteInj, finiteB634  have productA := cardinality.product_count with finiteInj, finiteA635  have coveredCount := cardinality.equipotent with (Finite.product with636    finiteInj, finiteA), (coveredPairs.equipotent at A, B)637  rw [sizeInj, sizeB] at productB638  rw [sizeInj, sizeA] at productA639  rw productA at coveredCount640  rw [productB, ← coveredCount] at split641  have natural := fallingFactorial.natural at n, m642  have natFresh := cardinality.nat with finiteFresh643  have freshCount : cardinality(freshPairs(A, B)) = fallingFactorial(n, m) * (n - m)644    rw mul.sub_distributes645    rw split646    symm647    exact sub.add_right at cardinality(freshPairs(A, B)), fallingFactorial(n, m) * m648  have finiteInsert := injections.finite with (Finite.insert at A, a with649    finiteA), finiteB650  have same := cardinality.equipotent with finiteInsert, (injections.insert_equipotent at A, B, a with fresh)651  rw [freshCount, ← fallingFactorial.succ] at same652  exact HasCardinality.of_cardinality with finiteInsert, same653654-- The number of injections from an m-element set into an n-element set.655theorem injections.cardinality (m : Nat)656  shows ∀ A, ∀ B, ∀ n, Nat(n) → HasCardinality(A, m) → HasCardinality(B, n) →657    HasCardinality(injections(A, B), fallingFactorial(n, m))658proof659  induction m660  | zero =>661    intros A B n nNat countedA countedB662    have empty := HasCardinality.empty_of_zero at A with countedA663    rw [empty, injections.empty_domain, fallingFactorial.zero]664    constructor665    . exact Naturals.constructor.succ at 0 with Naturals.constructor.zero666    . exact Equipotent.singleton_one at ∅667  | k + 1 using ih =>668    intros A B n nNat countedA countedB669    have hk : k + 1 = succ(k) := add.right_one with *670    rw hk at countedA671    obtain ⟨a, member⟩ := HasCardinality.exists_member with countedA672    have rest := HasCardinality.remove at A, a, k with countedA, member673    have fresh : ¬a ∈ A ∖ {a} by simp [difference.membership, singleton.membership]674    have restored := insert.restore with member675    have restCount := ih with A ∖ {a}, B, n, nNat, rest, countedB676    have inserted := injections.insert_count at A ∖ {a}, B, a, k, n with677      fresh, rest, countedB, restCount678    rw restored at inserted679    exact inserted680681theorem injections.count (A B : Set)682  requires finiteA : Finite(A)683  requires finiteB : Finite(B)684  shows685    cardinality(injections(A, B)) = fallingFactorial(cardinality(B), cardinality(A))686proof687  have countedA := cardinality.correct with finiteA688  have countedB := cardinality.correct with finiteB689  have natA := cardinality.nat with finiteA690  have natB := cardinality.nat with finiteB691  have all := injections.cardinality at cardinality(A)692  have counted := all with A, B, cardinality(B), natB, countedA, countedB693  exact cardinality.eq_of_has with counted694695theorem injections.count_self (A : Set)696  requires finite : Finite(A)697  shows cardinality(injections(A, A)) = cardinality(A)!698proof699  have count := injections.count with finite, finite700  have natA := cardinality.nat with finite701  rw [count, fallingFactorial.self]702  rfl703704theorem injections.empty_of_larger (A B : Set)705  requires finiteB : Finite(B)706  requires more : cardinality(B) < cardinality(A)707  shows injections(A, B) = ∅708proof709  apply Subset.empty_iff.forward710  intros f hf711  have injective := injections.injective with hf712  have function := Injective.function with injective713  exfalso714  exact pigeonhole.not_injective with function, finiteB, more, injective715716theorem injections.count_choose (A B : Set)717  requires finiteA : Finite(A)718  requires finiteB : Finite(B)719  requires le : cardinality(A) ≤ cardinality(B)720  shows721    cardinality(injections(A, B)) = (cardinality(B) choose cardinality(A)) * cardinality(A)!722proof723  have count := injections.count with finiteA, finiteB724  have natA := cardinality.nat with finiteA725  have natB := cardinality.nat with finiteB726  rw count727  exact fallingFactorial.choose with le728729-- Bijections between two sets, as a set of function graphs.730def bijections (A B : Set) : Set :=731  { f ∈ functionSpace(A, B) | BijectiveBetween(f, A, B) }732733theorem bijections.of_bijective (f A B : Set)734  requires bijective : BijectiveBetween(f, A, B)735  shows f ∈ bijections(A, B)736proof737  have function := Injective.function with (Bijective.injective with bijective)738  have inSpace := functionSpace.mem_iff.backward with function739  exact bijections.membership.backward with ⟨inSpace, bijective⟩740741theorem bijections.bijective (f A B : Set)742  requires member : f ∈ bijections(A, B)743  shows BijectiveBetween(f, A, B)744proof745  have parts := bijections.membership.forward with member746  exact parts.right747748theorem bijections.subset_injections (A B : Set)749  shows bijections(A, B) ⊆ injections(A, B)750proof751  intros f hf752  have bijective := bijections.bijective with hf753  exact injections.of_injective with (Bijective.injective with bijective)754755theorem bijections.finite (A B : Set)756  requires finiteA : Finite(A)757  requires finiteB : Finite(B)758  shows Finite(bijections(A, B))759proof760  have finite := injections.finite with finiteA, finiteB761  exact Finite.subset with finite, (bijections.subset_injections at A, B)762763-- Between finite sets of the same size every injection is a bijection.764theorem bijections.eq_injections (A B : Set)765  requires finiteB : Finite(B)766  requires same : cardinality(A) = cardinality(B)767  shows bijections(A, B) = injections(A, B)768proof769  apply Subset.antisymmetric with (bijections.subset_injections at A, B)770  intros f hf771  have injective := injections.injective with hf772  have bijective := Finite.bijective_of_injective with injective, finiteB, same773  exact bijections.of_bijective with bijective774775theorem bijections.count (A B : Set)776  requires finiteA : Finite(A)777  requires finiteB : Finite(B)778  requires same : cardinality(A) = cardinality(B)779  shows cardinality(bijections(A, B)) = cardinality(A)!780proof781  have equal := bijections.eq_injections with finiteB, same782  have count := injections.count with finiteA, finiteB783  have natA := cardinality.nat with finiteA784  rw [equal, count, ← same, fallingFactorial.self]785  rfl786787theorem bijections.count_self (A : Set)788  requires finite : Finite(A)789  shows cardinality(bijections(A, A)) = cardinality(A)!790proof791  have same : cardinality(A) = cardinality(A) by rfl792  exact bijections.count with finite, finite, same793794theorem bijections.empty_of_ne (A B : Set)795  requires finiteA : Finite(A)796  requires different : cardinality(A) ≠ cardinality(B)797  shows bijections(A, B) = ∅798proof799  apply Subset.empty_iff.forward800  intros f hf801  have bijective := bijections.bijective with hf802  exfalso803  apply different804  exact cardinality.bijective with finiteA, bijective805