OAI/Analysis/MarkovType/SubdivisionSpreading.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.Subdivision.extendPlacement line 9
2. theorem OAI.MarkovSuperreflexivity.Subdivision.extendPlacement_apply line 12
3. theorem OAI.MarkovSuperreflexivity.Subdivision.strictMono_extendPlacement line 16
4. theorem OAI.MarkovSuperreflexivity.Subdivision.mapDomain_ofArray line 29
5. theorem OAI.MarkovSuperreflexivity.Subdivision.mapDomain_extendPlacement line 35
6. theorem OAI.MarkovSuperreflexivity.Subdivision.norm_mapDomain line 45
7. theorem OAI.MarkovSuperreflexivity.Subdivision.uniform_spreading line 55