OAI/Analysis/JiangSu/Nonunital/QuotientSurjective.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalGamma.boundedInr line 16
  2. lemma OAI.NonunitalGamma.boundedInr_apply line 26
  3. lemma OAI.NonunitalGamma.boundedInr_norm line 29
  4. def OAI.NonunitalGamma.sequenceQuotientMap line 42
  5. lemma OAI.NonunitalGamma.sequenceQuotientMap_apply line 45
  6. lemma OAI.NonunitalGamma.sequenceQuotientMap_kernel line 49
  7. theorem OAI.NonunitalGamma.sequenceQuotientMap_bounded_lift line 57
  8. theorem OAI.NonunitalGamma.sequenceQuotientMap_surjective line 85
  9. lemma OAI.NonunitalGamma.hereditary_inr_map line 105
  10. lemma OAI.NonunitalGamma.positive_contraction_sequence_lift line 124
  11. theorem OAI.NonunitalGamma.projection_supply line 144