Finite Approximation Family

Abstract

The genuine continuous family (n,s) -> r_n(s), with infinity row s -> s, for the compatible finite approximations of an arbitrary light profinite S. Continuity is proved coordinatewise in the actual finite presentation: each projected family is eventually the projection itself as a continuous map, uniformly for all s. Empty, finite and infinite S are all allowed. New proofs, Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.1 (finite Approximation Family finite Slice).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationFamily.finiteApproximationFamily_finiteSlice

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The genuine continuous family (n,s) -> r_n(s), with infinity row s -> s, for the compatible finite approximations of an arbitrary light profinite S. Continuity is proved coordinatewise in the actual finite presentation: each projected family is eventually the projection itself as a continuous map, uniformly for all s. Empty, finite and infinite S are all allowed. New proofs, Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

Theorem 1.2 (finite Approximation Family infty Slice).

Lean statement: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationFamily.finiteApproximationFamily_inftySlice

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

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The genuine continuous family (n,s) -> r_n(s), with infinity row s -> s, for the compatible finite approximations of an arbitrary light profinite S. Continuity is proved coordinatewise in the actual finite presentation: each projected family is eventually the projection itself as a continuous map, uniformly for all s. Empty, finite and infinite S are all allowed. New proofs, Apache-2.0. Research construction: Juan Esteban Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.2.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationFamily.finiteApproximationFamily_finiteSlice
• Truth anchor: D5/S3/HomologicalAlgebra/Solid/FiniteApproximationFamily.finiteApproximationFamily_inftySlice
• Dependency: D5/S3/HomologicalAlgebra/Solid/FiniteApproximation