Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Approximation Selector

Abstract

The actual continuous pointed coefficient selector for the free-profinite generator retract. At finite row n it selects the code of (n, proj_n(s)); the infinity row is infinity. Every finite fiber is a clopen subset of a single finite row. This proves continuity for empty, finite and infinite S, without enumerating S by N or assuming derived realization. New proofs, Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.1 (finite Approximation Selector Fun fiber clopen).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationSelector.finiteApproximationSelectorFun_fiber_clopen

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual continuous pointed coefficient selector for the free-profinite generator retract. At finite row n it selects the code of (n, proj_n(s)); the infinity row is infinity. Every finite fiber is a clopen subset of a single finite row. This proves continuity for empty, finite and infinite S, without enumerating S by N or assuming derived realization. New proofs, Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.2 (finite Approximation Selector Fun continuous).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationSelector.finiteApproximationSelectorFun_continuous

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual continuous pointed coefficient selector for the free-profinite generator retract. At finite row n it selects the code of (n, proj_n(s)); the infinity row is infinity. Every finite fiber is a clopen subset of a single finite row. This proves continuity for empty, finite and infinite S, without enumerating S by N or assuming derived realization. New proofs, Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

References