OAI/MathematicalPhysics/AlternatingFlow/MachineProfiles.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AlternatingNS.Profiles.selector line 10
2. lemma OAI.AlternatingNS.Profiles.selector_smooth line 16
3. lemma OAI.AlternatingNS.Profiles.selector_nonneg line 20
4. lemma OAI.AlternatingNS.Profiles.selector_le_one line 23
5. lemma OAI.AlternatingNS.Profiles.selector_one line 27
6. lemma OAI.AlternatingNS.Profiles.selector_zero_left line 34
7. lemma OAI.AlternatingNS.Profiles.selector_zero_right line 38
8. lemma OAI.AlternatingNS.Profiles.selector_support_bound line 43
9. lemma OAI.AlternatingNS.Profiles.selector_support_disjoint line 51
10. lemma OAI.AlternatingNS.Profiles.selector_on_cell line 63
11. lemma OAI.AlternatingNS.Profiles.selector_code line 77
12. lemma OAI.AlternatingNS.Profiles.selector_streamCode line 87
13. lemma OAI.AlternatingNS.Machine.selector_recordedBlock line 101
14. lemma OAI.AlternatingNS.Machine.selector_leftCode line 109
15. lemma OAI.AlternatingNS.Machine.selector_rightCode line 118