Bounded Unit Map

Abstract

The canonical protected map q : P -> B_Z and its exact factorization of PToIntegerMeasures. All bounded test families have actual free maps to B_Z. New proofs, Apache-2.0; the concrete bounded intermediary is from Rodríguez Camargo’s Notes on Solid Geometry, Lemmas 3.3.3–3.3.4.

Theorem 1.1 (PTo Bounded Integer Measures comparison).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedUnitMap.PToBoundedIntegerMeasures_comparison

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/BoundedUnitMap.PToBoundedIntegerMeasures_comparison (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The canonical protected map q : P -> B_Z and its exact factorization of PToIntegerMeasures. All bounded test families have actual free maps to B_Z. New proofs, Apache-2.0; the concrete bounded intermediary is from Rodríguez Camargo’s Notes on Solid Geometry, Lemmas 3.3.3–3.3.4.

Theorem 1.2 (bounded Family Map range independent).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedUnitMap.boundedFamilyMap_range_independent

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/BoundedUnitMap.boundedFamilyMap_range_independent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The ordinary maps into B_Z do not depend on a presentation of the bound.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/BoundedUnitMap.PToBoundedIntegerMeasures_comparison
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/BoundedUnitMap.boundedFamilyMap_range_independent
• Dependency: D5/S3/HomologicalAlgebra/Solid/BoundedObject