OAI/Geometry/EinsteinFour/CoordinateConnectionUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The coordinate Levi-Civita coefficients are determined by torsion freeness and metric compatibility. This is the uniqueness step used when changing charts.

  1. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_eq_of_compatible line 19