ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates

4 sections | 4 files | 47 declarations

This aggregate collects the construction, equivalences, topology, and comparison formulas for closed-generated coordinates in completed Fox differential modules.

imports

Imported by

ProCGroups.FoxDifferential.Completed.Continuous

Basic

1 file | 16 declarations | 13 Theorems | 3 Definitions

The principal declarations in this module are: - `closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom` The closed-generated Fox vector, read as a crossed differen...

Comparison

1 file | 2 declarations | 2 Theorems

The principal declarations in this module are: - `continuous_familyCoordinatesZC_zcUnivDiff_of_closedGen_leftGraph` The paper coordinate universal differential is continuous onc...

Equiv

1 file | 20 declarations | 18 Theorems | 2 Definitions

The principal declarations in this module are: - `separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger` Coordinate equivalence for the separated completed differen...

Topology

1 file | 9 declarations | 8 Theorems | 1 Definition

The principal declarations in this module are: - `closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula` The coordinate topology on \(A_{\psi}(C)\) trans...