OAI/Analysis/SeparableQuotients/Positive/ScalarEvaluation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.Positive.Fields.Scalar.evaluation line 22
2. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.map_eq_of_spanVector line 24
3. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.evaluation_eq_prefix_at_normer line 34
4. def OAI.SeparableQuotient.Positive.Fields.Scalar.adjointPrefixVector line 47
5. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.adjointPrefixVector_bound line 51
6. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixCoord_adjointPrefixVector line 90
7. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.coefficient_pairing_adjointPrefixVector line 98
8. theorem OAI.SeparableQuotient.Positive.Fields.Scalar.prefix_evaluation_adjoint_lower line 113
9. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.closedSpan_separable line 139
10. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.prefixCoord_linearIndependent line 143
11. theorem OAI.SeparableQuotient.Positive.Fields.Scalar.prefix_evaluation_surjective line 159
12. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.mem_coefficient_span_of_summable line 186
13. theorem OAI.SeparableQuotient.Positive.Fields.Scalar.eval_range_of_dense_summable line 217