OAI/Geometry/EinsteinFour/WeightedAreaInequality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The noninjective change-of-variables inequality, with the target volume density retained. This is the local coordinate inequality needed for the exponential's image.

  1. theorem OAI.PositiveEinsteinFour.Geometry.weighted_area_inequality line 17