OAI/Analysis/MarkovType/NormedC00.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.NormedC00 line 9
2. instance OAI.MarkovSuperreflexivity.NormedC00.(instance at line 15) line 15
3. instance OAI.MarkovSuperreflexivity.NormedC00.(instance at line 17) line 17
4. instance OAI.MarkovSuperreflexivity.NormedC00.(instance at line 19) line 19
5. theorem OAI.MarkovSuperreflexivity.NormedC00.normCore line 21
6. instance OAI.MarkovSuperreflexivity.NormedC00.(instance at line 29) line 29
7. instance OAI.MarkovSuperreflexivity.NormedC00.(instance at line 32) line 32
8. def OAI.MarkovSuperreflexivity.NormedC00.coefficients line 35
9. theorem OAI.MarkovSuperreflexivity.NormedC00.norm_eq line 37
10. abbrev OAI.MarkovSuperreflexivity.OrderedSpace line 41