OAI/Analysis/WeakInfiniteness/ColumnNormalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.columnMetricFunction line 29
  2. def OAI.WeakPureInfiniteness.columnCoreFunction line 31
  3. lemma OAI.WeakPureInfiniteness.continuous_columnMetricFunction line 33
  4. lemma OAI.WeakPureInfiniteness.continuous_columnCoreFunction line 39
  5. lemma OAI.WeakPureInfiniteness.columnMetricFunction_nonneg line 43
  6. lemma OAI.WeakPureInfiniteness.columnMetricFunction_bound line 46
  7. lemma OAI.WeakPureInfiniteness.columnMetricFunction_scalar line 50
  8. lemma OAI.WeakPureInfiniteness.column_left_normalization line 67