OAI/Dynamics/StandardMap/EndpointDefinition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.leftEndpoint line 12
2. def OAI.StandardMapEntropy.rightEndpoint line 14
3. lemma OAI.StandardMapEntropy.measurable_leftEndpoint line 16
4. lemma OAI.StandardMapEntropy.measurable_rightEndpoint line 21
5. lemma OAI.StandardMapEntropy.leftEndpoint_le_of_nonunit line 26
6. lemma OAI.StandardMapEntropy.le_rightEndpoint_of_nonunit line 30
7. lemma OAI.StandardMapEntropy.le_leftEndpoint_iff line 34
8. lemma OAI.StandardMapEntropy.rightEndpoint_le_iff line 42
9. lemma OAI.StandardMapEntropy.leftEndpoint_lower_ray line 50
10. lemma OAI.StandardMapEntropy.rightEndpoint_upper_ray line 59