Grace/Cumulus/Cardinal/FiniteUnion.g17

Imports

Declarations

union.insert theorem derivation
listSupport.finite_union theorem derivation
Finite.big_union theorem derivation

Source

1-- A finite union of finite sets is finite, in ZF without a choice function.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.FiniteUnion8import ListSupport910theorem union.insert (A S : Set)11  shows ⋃insert(S, A) = S ∪ ⋃A12proof13  ext y14  simp [set.union, insert.membership, union2.membership]1516theorem listSupport.finite_union (A : Set) (xs : List(A))17  requires members : ∀ S ∈ A, Finite(S)18  shows Finite(⋃listSupport{A}(xs))19proof20  induction xs21  | List.nil =>22    rw listSupport.nil23    have bounded : ⋃∅ ⊆ ∅ by simp [Subset, set.union, set.empty]24    exact Finite.subset with Finite.empty, bounded25  | List.cons(S, tail) using ih =>26    have member : S ∈ A by assumption27    have finite := members with S, member28    rw [listSupport.cons, union.insert]29    exact Finite.union with finite, ih3031theorem Finite.big_union (A : Set)32  requires finite : Finite(A)33  requires members : ∀ S ∈ A, Finite(S)34  shows Finite(⋃A)35proof36  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite37  have bound := listSupport.finite_union with *38  have included : ⋃A ⊆ ⋃listSupport{A}(xs)39    intros x hx40    obtain ⟨S, member, inS⟩ := set.union.forward with hx41    have supported := covers with S, member42    exact union.contains with supported, inS43  exact Finite.subset with bound, included44