Grace/Cumulus/Cardinal/FiniteImage.g17

Imports

Declarations

listSupport.image_cover theorem derivation
Finite.function_image theorem derivation
Source

1-- Images of finite sets are finite, without Choice.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.FiniteImage8import ListSupport910theorem listSupport.image_cover (D C f : Set) (xs : List(D))11  requires function : f : D → C12  shows ∃ ys, List(C, ys) ∧ (∀ x ∈ listSupport{D}(xs), f(x) ∈ listSupport{C}(ys))13proof14  induction xs15  | List.nil =>16    have nil : List(C, []) by typecheck17    refine ⟨[], nil, _⟩18    intros x hx19    unfold listSupport at hx20    exfalso21    exact set.empty with hx22  | List.cons(x, tail) using ih =>23    obtain ⟨ys, listY, covers⟩ := ih24    have value := FunctionBetween.apply_closed with *25    have next : List(C, f(x) :: ys) by typecheck26    refine ⟨f(x) :: ys, next, _⟩27    intros y hy28    rw listSupport at hy29    have casesY := insert.membership.forward with hy30    rw listSupport31    cases casesY with same | old32    . rw same33      exact insert.self34    . have previous := covers with y, old35      exact insert.contains with previous3637theorem Finite.function_image (D C f S : Set)38  requires function : f : D → C39  requires finite : Finite(S)40  requires subset : S ⊆ D41  shows Finite(functionImage(f, S, C))42proof43  obtain ⟨xs, listX, covers⟩ := Finite.cover_in with finite, subset44  obtain ⟨ys, listY, values⟩ := listSupport.image_cover at D, C, f, xs with *45  have finiteY := listSupport.finite at C, ys with *46  have bounded : functionImage(f, S, C) ⊆ listSupport{C}(ys)47    intros y hy48    obtain ⟨inC, x, hx, equation⟩ := functionImage.membership.forward with hy49    have covered := covers with x, hx50    have value := values with x, covered51    rwa equation52  exact Finite.subset with finiteY, bounded53