OAI/Analysis/SeparableQuotients/Positive/DualSequences.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.Positive.Fields.chooseUnitVector line 16
  2. lemma OAI.SeparableQuotient.Positive.Fields.chooseUnitVector_spec line 20
  3. def OAI.SeparableQuotient.Positive.Fields.normerState line 27
  4. def OAI.SeparableQuotient.Positive.Fields.selectedVector line 36
  5. def OAI.SeparableQuotient.Positive.Fields.selectedNormers line 40
  6. lemma OAI.SeparableQuotient.Positive.Fields.normerState_value line 44
  7. lemma OAI.SeparableQuotient.Positive.Fields.normerState_mono line 56
  8. lemma OAI.SeparableQuotient.Positive.Fields.selectedNormers_subset_state line 63
  9. lemma OAI.SeparableQuotient.Positive.Fields.selectedVector_norm line 71
  10. lemma OAI.SeparableQuotient.Positive.Fields.selectedVector_ann_test line 76
  11. lemma OAI.SeparableQuotient.Positive.Fields.selectedVector_ann_normers line 86
  12. theorem OAI.SeparableQuotient.Positive.Fields.exists_normed_prefix_sequence line 96
  13. def OAI.SeparableQuotient.Positive.Fields.HasSeparableQuotient line 125