module
module
IndisputableMonolith.Gravity.RestrictedIncidenceRecovery
show as:
view Lean formalization →
depends on (1)
declarations in this module (11)
-
abbrev
DeficitSubspace -
def
RestrictedIncidenceDeficitSeparating -
def
RestrictedIncidenceDeficitRecovering -
theorem
restrictedIncidenceDeficitSeparating_of_recovering -
def
RecoverableDeficitSubspace -
theorem
restrictedRecovering_recoverableSubspace -
theorem
restrictedSeparating_recoverableSubspace -
def
DirectionalLengthImageSubspace -
theorem
directionalLengthImageSubspace_separating -
theorem
zero_deficit_of_critical_of_restrictedVariationFormula -
def
discreteVacuumEinsteinInput_of_restrictedRecovery