OAI/Analysis/SeparableQuotients/Positive/RowBasis.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeparableQuotient.Positive.Rows.ClosedSpan line 14
  2. def OAI.SeparableQuotient.Positive.Rows.spanVector line 17
  3. def OAI.SeparableQuotient.Positive.Rows.spanCombination line 20
  4. lemma OAI.SeparableQuotient.Positive.Rows.spanCombination_coe line 23
  5. lemma OAI.SeparableQuotient.Positive.Rows.denseRange_spanCombination line 27
  6. def OAI.SeparableQuotient.Positive.Rows.PrefixBoundTwo line 42
  7. lemma OAI.SeparableQuotient.Positive.Rows.prefix_coefficient_bound line 46
  8. def OAI.SeparableQuotient.Positive.Rows.prefixCoord line 62
  9. lemma OAI.SeparableQuotient.Positive.Rows.prefixCoord_combination line 65
  10. lemma OAI.SeparableQuotient.Positive.Rows.prefixCoord_bound line 71
  11. lemma OAI.SeparableQuotient.Positive.Rows.prefixCoord_ortho line 77
  12. def OAI.SeparableQuotient.Positive.Rows.prefixProjection line 86
  13. lemma OAI.SeparableQuotient.Positive.Rows.prefixProjection_apply line 90
  14. lemma OAI.SeparableQuotient.Positive.Rows.prefixProjection_bound line 94
  15. lemma OAI.SeparableQuotient.Positive.Rows.prefixProjection_combination line 108
  16. lemma OAI.SeparableQuotient.Positive.Rows.prefix_expansion line 116
  17. def OAI.SeparableQuotient.Positive.Rows.basisOfPrefix line 140
  18. lemma OAI.SeparableQuotient.Positive.Rows.prefixBound_of_half_normers line 166