OAI/Analysis/MarkovType/SubdivisionProfileDefs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.Subdivision.ofList line 10
2. theorem OAI.MarkovSuperreflexivity.Subdivision.ofList_ofFn line 13
3. def OAI.MarkovSuperreflexivity.Subdivision.pieces line 18
4. theorem OAI.MarkovSuperreflexivity.Subdivision.pieces_nil line 21
5. theorem OAI.MarkovSuperreflexivity.Subdivision.pieces_cons line 23
6. def OAI.MarkovSuperreflexivity.Subdivision.finiteSubdivision line 26