Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation

Abstract

Compatible finite-image retractions for every light profinite space, using the actual pinned sequential finite presentation. The choices work also for empty and finite spaces; no enumeration of the represented points by N is asserted. These are the finite-approximation data needed for the concrete generator retract in Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. New proofs, Apache-2.0.

Theorem 1.1 (finite Approximation range finite).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximation.finiteApproximation_range_finite

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Compatible finite-image retractions for every light profinite space, using the actual pinned sequential finite presentation. The choices work also for empty and finite spaces; no enumeration of the represented points by N is asserted. These are the finite-approximation data needed for the concrete generator retract in Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. New proofs, Apache-2.0.

Theorem 1.2 (finite Approximation ranges monotone).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximation.finiteApproximation_ranges_monotone

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. Compatible finite-image retractions for every light profinite space, using the actual pinned sequential finite presentation. The choices work also for empty and finite spaces; no enumeration of the represented points by N is asserted. These are the finite-approximation data needed for the concrete generator retract in Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2. New proofs, Apache-2.0.

References

  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximation.finiteApproximation_range_finite
  • Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximation.finiteApproximation_ranges_monotone