OAI/Geometry/PrescribedPotential/MatrixLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Matrix Limit.

  1. lemma OAI.CompactMatrixPositivity.posSemidef_of_tendsto line 19
  2. lemma OAI.CompactMatrixPositivity.posDef_of_tendsto_det_ne_zero line 32