OAI/Analysis/SeparableQuotients/Positive/ScalarQuotients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SeparableQuotient.Positive.Fields.Scalar.quotient_of_separable_evaluation line 22
2. theorem OAI.SeparableQuotient.Positive.Fields.exists_separable_closed_infinite_subspace line 78
3. theorem OAI.SeparableQuotient.Positive.Fields.infiniteDimensional_strongDual line 103
4. lemma OAI.SeparableQuotient.Positive.Fields.Scalar.dual_lower_of_surjective line 129
5. theorem OAI.SeparableQuotient.Positive.Fields.Scalar.separable_evaluation_of_quotient line 143
6. theorem OAI.SeparableQuotient.Positive.Fields.Scalar.evaluation_criterion line 178