HartogsStarter

Hartogs' theorem in ZF: every set is smaller than some ordinal

Open in Workbench View on GitHub

1-- Hartogs' theorem in ZF: every set is smaller than some ordinal.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 HartogsStarter8import Grace.Cumulus.Cardinal910-- No well-ordering of A, and no Choice assumption, is needed.11theorem larger_ordinal (A : Set)12  shows ∃ α, α ∈ Ordinal ∧ (∀ f, ¬InjectiveBetween(f, α, A))13proof14  exact Hartogs.theorem1516-- The explicit constructed ordinal cannot be injected into A.17theorem no_injection (A f : Set)18  shows ¬InjectiveBetween(f, hartogsBound(A), A)19proof20  exact hartogsBound.no_injection2122-- Well-orders can be transported to the image of any injection.23theorem transport (f A B r : Set)24  requires injective : InjectiveBetween(f, A, B)25  requires order : WellOrder(A, r)26  shows WellOrder(functionImage(f, A, B), transportedOrder(f, A, B, r))27proof28  exact transportedOrder.well_order at f, A, B, r with *29