OAI/Analysis/MarkovType/FiniteCharts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MarkovSuperreflexivity.Chart line 9
2. instance OAI.MarkovSuperreflexivity.chartFintype line 11
3. def OAI.MarkovSuperreflexivity.Chart.Good line 21
4. theorem OAI.MarkovSuperreflexivity.Chart.good_symm_iff line 24
5. theorem OAI.MarkovSuperreflexivity.Chart.good_rank line 46
6. theorem OAI.MarkovSuperreflexivity.Chart.rank_lt line 51