Grace/Cumulus/Set/ChoiceFunctions.g17

Open in Workbench Download source

Imports

Core

Declarations

• inhabitedSubsets def
• SubsetChoice predicate
• SubsetChoice.exists theorem derivation
• SubsetChoice.member theorem derivation

Source

1-- Set-sized selection from the axiom of choice, without global 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 Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module Grace.Cumulus.Set.ChoiceFunctions9import Core1011def inhabitedSubsets (A : Set) : Set := {S ∈ 𝒫(A) | Nonempty(S)}12predicate SubsetChoice (c A : Set) := ∀ S ∈ 𝒫(A), Nonempty(S) → c[S] ∈ S1314theorem SubsetChoice.exists (A : Set)15  shows ∃ c, SubsetChoice(c, A)16proof17  have inhabited : ∀ S ∈ inhabitedSubsets(A), ∃ x, x ∈ S18    intros S member19    obtain ⟨subset, nonempty⟩ := inhabitedSubsets.membership.forward with member20    exact nonempty21  obtain ⟨c, function, selects⟩ := set.choice with inhabited22  witness c23  intros S subset nonempty24  have member : S ∈ inhabitedSubsets(A) := inhabitedSubsets.membership.backward with ⟨subset, nonempty⟩25  exact selects with S, member2627theorem SubsetChoice.member (c A S : Set)28  requires choice : SubsetChoice(c, A)29  requires subset : S ⊆ A30  requires inhabited : Nonempty(S)31  shows c[S] ∈ S32proof33  unfold Subset at subset34  have bounded := set.powerset.backward with subset35  exact choice with S, bounded, inhabited36