OAI/Analysis/CharacterCriterion/Fullness.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.quotientNormedAlgebra line 22
  2. def OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.quotientCLM line 25
  3. lemma OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.quotientCLM_apply line 31
  4. lemma OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.quotient_norm_one line 33
  5. def OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.stateFace line 40
  6. lemma OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.stateFace_compact line 43
  7. lemma OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.stateFace_nonempty line 50
  8. lemma OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.stateFace_isFace line 73
  9. theorem OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.exists_pure_annihilating line 107
  10. lemma OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.pureRepresentation_annihilates line 117
  11. theorem OAI.KirchbergRordam.GenericRW.PrimitiveSeparation.exists_irreducible_annihilating line 135
  12. def OAI.KirchbergRordam.GenericRW.Fullness.closedIdeal line 148
  13. instance OAI.KirchbergRordam.GenericRW.Fullness.closedIdeal_twoSided line 150
  14. instance OAI.KirchbergRordam.GenericRW.Fullness.closedIdeal_isClosed line 156
  15. lemma OAI.KirchbergRordam.GenericRW.Fullness.eq_top_of_closedIdeal_eq_top line 159
  16. def OAI.KirchbergRordam.GenericRW.Fullness.IsFull line 176
  17. lemma OAI.KirchbergRordam.GenericRW.Fullness.full_iff_closed line 178
  18. lemma OAI.KirchbergRordam.GenericRW.Fullness.full_of_survives line 188
  19. lemma OAI.KirchbergRordam.GenericRW.Fullness.full_ne_zero line 198
  20. lemma OAI.KirchbergRordam.GenericRW.Fullness.full_survives line 207
  21. lemma OAI.KirchbergRordam.GenericRW.Fullness.bridges_span_one line 218
  22. lemma OAI.KirchbergRordam.GenericRW.Fullness.mem_span_finite line 245