OAI/Geometry/EinsteinFour/CompactDomination.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness passes to a linear map whose norm is controlled by a compact map. This is used for the finite coordinate reconstruction of two-forms.

  1. theorem OAI.PositiveEinsteinFour.Geometry.compact_of_norm_domination line 14
  2. theorem OAI.PositiveEinsteinFour.Geometry.compact_finite_pi line 55