Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Bounded Measure Naturality

Abstract

Naturality of the actual bounded-family lift and independence of its finite coefficient range. New proofs, Apache-2.0. The free-tensor naturality proof is the right-variable companion to the attributed freeTensorIsoInt proof in DiscreteInt, using the official Mathlib monoidal APIs.

Theorem 1.1 (bounded Coefficient Map range independent).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedMeasureNaturality.boundedCoefficientMap_range_independent

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Naturality of the actual bounded-family lift and independence of its finite coefficient range. New proofs, Apache-2.0. The free-tensor naturality proof is the right-variable companion to the attributed freeTensorIsoInt proof in DiscreteInt, using the official Mathlib monoidal APIs.

Theorem 1.2 (bounded Family Local Lift range independent).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedMeasureNaturality.boundedFamilyLocalLift_range_independent

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Naturality of the actual bounded-family lift and independence of its finite coefficient range. New proofs, Apache-2.0. The free-tensor naturality proof is the right-variable companion to the attributed freeTensorIsoInt proof in DiscreteInt, using the official Mathlib monoidal APIs.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/BoundedMeasureNaturality.boundedCoefficientMap_range_independent
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/BoundedMeasureNaturality.boundedFamilyLocalLift_range_independent
  • Dependency: D5/S3/HomologicalAlgebra/Solid/MeasureFactorization