OAI/Analysis/SeparableQuotients/Positive/RowEvaluation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.Positive.Rows.evaluation line 21
  2. lemma OAI.SeparableQuotient.Positive.Rows.map_eq_of_spanVector line 23
  3. lemma OAI.SeparableQuotient.Positive.Rows.evaluation_eq_prefix_at_normer line 33
  4. theorem OAI.SeparableQuotient.Positive.Rows.prefix_evaluation_adjoint_lower line 47
  5. lemma OAI.SeparableQuotient.Positive.Rows.closedSpan_separable line 112
  6. lemma OAI.SeparableQuotient.Positive.Rows.prefixCoord_linearIndependent line 116
  7. theorem OAI.SeparableQuotient.Positive.Rows.prefix_evaluation_surjective line 132
  8. lemma OAI.SeparableQuotient.Positive.Rows.mem_coefficient_span_of_summable line 159
  9. theorem OAI.SeparableQuotient.Positive.Rows.eval_range_of_dense_summable line 190