OAI/Analysis/MarkovType/OrderedNorm.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MarkovSuperreflexivity.OrderedNorm line 9
2. instance OAI.MarkovSuperreflexivity.OrderedNorm.(instance at line 18) line 18
3. theorem OAI.MarkovSuperreflexivity.OrderedNorm.coe_toSeminorm line 20
4. theorem OAI.MarkovSuperreflexivity.OrderedNorm.map_zero line 23
5. theorem OAI.MarkovSuperreflexivity.OrderedNorm.nonneg line 26
6. theorem OAI.MarkovSuperreflexivity.OrderedNorm.eq_zero_iff line 29
7. theorem OAI.MarkovSuperreflexivity.OrderedNorm.add_le line 32
8. theorem OAI.MarkovSuperreflexivity.OrderedNorm.neg line 35
9. theorem OAI.MarkovSuperreflexivity.OrderedNorm.smul line 38
10. def OAI.MarkovSuperreflexivity.CoordinatesRepresentable line 47