Grace/Cumulus/Geometry/Absorption.g17

Open in Workbench Download source

Imports

Absorption.CountableUnion · Absorption.Absorb · Absorption.Triples · Absorption.Turn · Absorption.Roots · Absorption.Order · Absorption.TurnRotation · Absorption.Separation · Absorption.Sphere · Absorption.Pieces · Absorption.Final

Declarations

Source

1-- Absorbing countable sets: countable unions, the absorption theorem for a2-- group action, the rational rotations turn(t) about the z-axis, their3-- membership in SO3, the countability of the parameters t at which turn(t)4-- has finite order, and the separation of a countable subset of the5-- sphere from itself by some turn(t)6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Geometry.Absorption12import Absorption.CountableUnion13import Absorption.Absorb14import Absorption.Triples15import Absorption.Turn16import Absorption.Roots17import Absorption.Order18import Absorption.TurnRotation19import Absorption.Separation20import Absorption.Sphere21import Absorption.Pieces22import Absorption.Final23