Grace/Cumulus/List/ConsImage.g17

Open in Workbench Download source

Imports

Basic · Cardinal.NaturalSum

Declarations

• consMap defgraph
• consMap.injective theorem derivation
• consMap.image theorem derivation
• consImage.finite theorem derivation
• consImage.cardinality theorem derivation

Source

1-- Prepending a fixed entry to the lists of a set is an injection, so a2-- cons image of a finite set is finite and has the size of its source3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.List.ConsImage9import Basic10import Cardinal.NaturalSum1112-- The cons map ys ↦ x :: ys onto the cons image.13defgraph consMap (x S : Set) (ys ∈ S) : consImage(x, S) := x :: ys14proof15  apply consImage.membership.backward16  refine ⟨ys, member, rfl⟩1718theorem consMap.injective (x S : Set)19  shows InjectiveBetween(consMap(x, S), S, consImage(x, S))20proof21  have function := consMap.function at x, S22  constructor23  . exact function24  . intros u hu v hv z hz huz hvz25    have uValue := FunctionBetween.apply_value with function, hu, huz26    have vValue := FunctionBetween.apply_value with function, hv, hvz27    have uShape := consMap.value at x, S, u with hu28    have vShape := consMap.value at x, S, v with hv29    have equal : x :: u = x :: v30      rw [← uShape, ← vShape, uValue, vValue]31      rfl32    have parts := List.inductive.injective.cons with equal33    exact parts.right3435theorem consMap.image (x S : Set)36  shows functionImage(consMap(x, S), S, consImage(x, S)) = consImage(x, S)37proof38  ext zs39  constructor40  . intro hz41    have parts := functionImage.membership.forward with hz42    exact parts.left43  . intro hz44    obtain ⟨ys, hy, shape⟩ := consImage.membership.forward with hz45    apply functionImage.membership.backward46    constructor47    . exact hz48    . witness ys49      constructor50      . exact hy51      . rw ← shape52        symm53        exact consMap.value at x, S, ys with hy5455theorem consImage.finite (x S : Set)56  requires finite : Finite(S)57  shows Finite(consImage(x, S))58proof59  have function := consMap.function at x, S60  have reflexive := Subset.reflexive at S61  have image := Finite.function_image with function, finite, reflexive62  rwa consMap.image at image6364theorem consImage.cardinality (x S : Set)65  requires finite : Finite(S)66  shows cardinality(consImage(x, S)) = cardinality(S)67proof68  have injective := consMap.injective at x, S69  have reflexive := Subset.reflexive at S70  have image := cardinality.injective_image with injective, reflexive, finite71  rwa consMap.image at image72