-- Arbitrary selection, isolated from the ZF set library.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.
module Grace.Cumulus.Set.Choice
import Core

-- Global choice is exposed through this interface:
-- choosing from an inhabited set returns one of its members.
theorem choose.member (A : Set)
  requires inhabited : Nonempty(A)
  shows choose(A) ∈ A
proof
  simp [Nonempty.ne_empty, set.globalChoice]