Grace/Cumulus/Set/Choice.g17

Open in Workbench Download source

Imports

Core

Declarations

• choose.member theorem derivation

Source

1-- Arbitrary selection, isolated from the ZF set library.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.Choice9import Core1011-- Global choice is exposed through this interface:12-- choosing from an inhabited set returns one of its members.13theorem choose.member (A : Set)14  requires inhabited : Nonempty(A)15  shows choose(A) ∈ A16proof17  simp [Nonempty.ne_empty, set.globalChoice]18