OAI/Combinatorics/HadwigerCounterexample/ResponseSolvability.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HadwigerCounterexample.Individual line 13
2. abbrev OAI.HadwigerCounterexample.OnForms line 14
3. abbrev OAI.HadwigerCounterexample.ReqF line 15
4. def OAI.HadwigerCounterexample.combineF line 17
5. theorem OAI.HadwigerCounterexample.combineF_val line 26
6. theorem OAI.HadwigerCounterexample.combineF_single line 30
7. theorem OAI.HadwigerCounterexample.combineF_same line 37
8. def OAI.HadwigerCounterexample.obsPair line 47
9. theorem OAI.HadwigerCounterexample.obsPair_val line 50
10. def OAI.HadwigerCounterexample.eachF line 59

    Source documentation

    Restrict pure form to individual diagonal blocks.

    def eachF (p : Shape) {n} :
        PureForms p n →ₗ[F] Individual p n where
    …

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.PureForms, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Individual

11. def OAI.HadwigerCounterexample.sumF line 66

    Source documentation

    Extend the individual forms by zero outside respective blocks, then add.

    def sumF (p : Shape) {n} : Individual p n → PureForms p n :=
    …

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Individual, OAI.HadwigerCounterexample.PureForms

12. theorem OAI.HadwigerCounterexample.each_sumF line 68
13. def OAI.HadwigerCounterexample.repF line 81
14. theorem OAI.HadwigerCounterexample.repF_rep line 84
15. theorem OAI.HadwigerCounterexample.obsPair_each line 89
16. theorem OAI.HadwigerCounterexample.obsPair_chan line 101
17. theorem OAI.HadwigerCounterexample.each_chan_val line 109
18. theorem OAI.HadwigerCounterexample.obsPair_chan_change line 114
19. theorem OAI.HadwigerCounterexample.react_obsPair line 124
20. def OAI.HadwigerCounterexample.Volley.demand line 132
21. theorem OAI.HadwigerCounterexample.Volley.realize_linear line 135