OAI/Analysis/SeparableQuotients/Positive/ScalarBasis.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeparableQuotient.Positive.Fields.Scalar.ClosedSpan line 15
  2. def OAI.SeparableQuotient.Positive.Fields.Scalar.spanVector line 18
  3. def OAI.SeparableQuotient.Positive.Fields.Scalar.spanCombination line 21
  4. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.spanCombination_coe line 24
  5. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.denseRange_spanCombination line 28
  6. def OAI.SeparableQuotient.Positive.Fields.Scalar.PrefixBoundTwo line 43
  7. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefix_coefficient_bound line 47
  8. def OAI.SeparableQuotient.Positive.Fields.Scalar.prefixCoord line 63
  9. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixCoord_combination line 66
  10. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixCoord_bound line 72
  11. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixCoord_ortho line 78
  12. def OAI.SeparableQuotient.Positive.Fields.Scalar.prefixProjection line 87
  13. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixProjection_apply line 91
  14. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixProjection_bound line 95
  15. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixProjection_combination line 109
  16. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefix_expansion line 117
  17. def OAI.SeparableQuotient.Positive.Fields.Scalar.basisOfPrefix line 141
  18. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixBound_of_half_normers line 168