Grace/Cumulus.g17

Open in Workbench Download source

Imports

Real · Rat · Cardinal · Order · Ordinal · Set.MaximalPrinciple · Set.WellOrdering · Cardinal.Infinite · Cardinal.Algebra · Cardinal.Square · Cardinal.Combinations · List · Topology · FixedPoint · Algebra.Ring.MaximalIdeal · NumberTheory · Algebra · LinearAlgebra · GraphTheory · GraphTheory.Friendship · GraphTheory.DoubleCover.Theorem · GameTheory · Geometry · Geometry.Absorption · Complex · Complex.Nullstellensatz · Complex.Cubic · Complex.Quartic · Complex.FundamentalTheoremGeneral · Lattice · Combinatorics · Category · Probability · Metric · Rotation · Geometry.Hausdorff · Geometry.Sphere · Geometry.BanachTarski · Geometry.BanachTarski.Strong

Declarations

Source

1-- The Cumulus mathematics library2-- 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 Grace.Cumulus8import Real9import Rat10import Cardinal11import Order12import Ordinal13import Set.MaximalPrinciple14import Set.WellOrdering15import Cardinal.Infinite16import Cardinal.Algebra17import Cardinal.Square18import Cardinal.Combinations19import List20import Topology21import FixedPoint22import Algebra.Ring.MaximalIdeal23import NumberTheory24import Algebra25import LinearAlgebra26import GraphTheory27-- The friendship theorem's modules reach the choice axiom only through the28-- Combinatorics area's imports, so they join the library here rather than29-- in the GraphTheory root, which stays available under ZF.30import GraphTheory.Friendship31-- The cycle double cover theorem chooses base sums and cycle decompositions32-- through Set.Choice, so its last modules join the library here rather than33-- in the GraphTheory root, which stays available under ZF.34import GraphTheory.DoubleCover.Theorem35import GameTheory36import Geometry37-- The absorption layer of the Banach–Tarski development uses the choice38-- axiom through Set.Choice, so it joins the library here rather than in39-- the Geometry root, which stays available under ZF.40import Geometry.Absorption41import Complex42import Complex.Nullstellensatz43import Complex.Cubic44import Complex.Quartic45import Complex.FundamentalTheoremGeneral46import Lattice47import Combinatorics48import Category49import Probability50import Metric51import Rotation52import Geometry.Hausdorff53import Geometry.Sphere54import Geometry.BanachTarski55import Geometry.BanachTarski.Strong5657-- GRACE17 Cumulus: reusable, kernel-checked mathematics over sets.58