OAI/Probability/Ballisticity/Stationary/ArrayTopology.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DirectionalTransience.StationaryCompact.discreteOnePoint_countable line 12
2. instance OAI.DirectionalTransience.StationaryCompact.discreteOnePoint_firstCountable line 16
3. instance OAI.DirectionalTransience.StationaryCompact.discreteOnePoint_secondCountable line 31
4. abbrev OAI.DirectionalTransience.StationaryCompact.Label line 34
5. abbrev OAI.DirectionalTransience.StationaryCompact.MarkSpace line 35
6. abbrev OAI.DirectionalTransience.StationaryCompact.EpisodeArray line 36
7. instance OAI.DirectionalTransience.StationaryCompact.array_compact line 45
8. instance OAI.DirectionalTransience.StationaryCompact.array_secondCountable line 46
9. instance OAI.DirectionalTransience.StationaryCompact.array_t2 line 47
10. instance OAI.DirectionalTransience.StationaryCompact.array_metrizable line 52
11. def OAI.DirectionalTransience.StationaryCompact.shift line 54
12. lemma OAI.DirectionalTransience.StationaryCompact.shift_continuous line 62