OAI/Analysis/CharacterCriterion/ConeModel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.KirchbergRordam.GenericRW.ConeModel.coneSubringClass line 27
2. instance OAI.KirchbergRordam.GenericRW.ConeModel.(instance at line 31) line 31
3. def OAI.KirchbergRordam.GenericRW.ConeModel.scalar line 33
4. lemma OAI.KirchbergRordam.GenericRW.ConeModel.scalar_apply line 44
5. abbrev OAI.KirchbergRordam.GenericRW.ConeModel.tip line 47
6. lemma OAI.KirchbergRordam.GenericRW.ConeModel.tip_selfAdjoint line 48
7. lemma OAI.KirchbergRordam.GenericRW.ConeModel.scalar_continuous line 53
8. def OAI.KirchbergRordam.GenericRW.ConeModel.entry line 59
9. lemma OAI.KirchbergRordam.GenericRW.ConeModel.entry_continuous line 65
10. lemma OAI.KirchbergRordam.GenericRW.ConeModel.scalar_tip_mem line 70
11. def OAI.KirchbergRordam.GenericRW.ConeModel.entryWeight line 94
12. lemma OAI.KirchbergRordam.GenericRW.ConeModel.weight_zero line 97
13. def OAI.KirchbergRordam.GenericRW.ConeModel.fromWeight line 101
14. lemma OAI.KirchbergRordam.GenericRW.ConeModel.fromWeight_continuous line 104
15. lemma OAI.KirchbergRordam.GenericRW.ConeModel.entry_tip_mem line 108
16. lemma OAI.KirchbergRordam.GenericRW.ConeModel.vanish_one_mem line 144
17. lemma OAI.KirchbergRordam.GenericRW.IntervalCalculus.ext_coord line 181
18. lemma OAI.KirchbergRordam.GenericRW.ConeModel.scalar_coord line 207
19. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coneHom_scalar line 225
20. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coneHom_tip line 234
21. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.coneHom_hereditary line 237
22. def OAI.KirchbergRordam.GenericRW.ConeModel.defectSubalgebra line 254
23. abbrev OAI.KirchbergRordam.GenericRW.ConeModel.Defect line 262
24. instance OAI.KirchbergRordam.GenericRW.ConeModel.defectZero line 263
25. instance OAI.KirchbergRordam.GenericRW.ConeModel.defectClosed line 265
26. instance OAI.KirchbergRordam.GenericRW.ConeModel.(instance at line 267) line 267
27. def OAI.KirchbergRordam.GenericRW.ConeModel.toHereditary line 270
28. def OAI.KirchbergRordam.GenericRW.ConeModel.scalarDefect line 279
29. def OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.defectHom line 289
30. lemma OAI.KirchbergRordam.GenericRW.SquareZeroCone.WeightedMatrix.defectHom_scalar line 298