ZornStarter

Ordinary Choice is sufficient: check this example with --foundation ZFC

Open in Workbench View on GitHub

1-- Ordinary Choice is sufficient: check this example with --foundation ZFC.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 ZornStarter8import Grace.Cumulus.Set.Zorn910theorem maximal_element (A r : Set)11  requires order : IsPartialOrder(A, r)12  requires bounds : ∀ C, Chain(A, r, C) → ∃ u, UpperBound(A, r, C, u)13  shows ∃ m, Maximal(A, r, m)14proof15  have condition : ZornCondition(A, r)16    unfold ZornCondition17    refine ⟨order, bounds⟩18  exact Zorn.theorem with condition1920-- The inclusion poset of chains supplies the first reusable application.21theorem maximal_chain (A r : Set)22  shows ∃ C, Chain(A, r, C) ∧ (∀ D, Chain(A, r, D) → C ⊆ D → D = C)23proof24  exact Chain.exists_maximal25