OAI/Combinatorics/HadwigerCounterexample/BinaryEvaluationForms.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.pullT line 13
2. theorem OAI.HadwigerCounterexample.indexed_linear line 18
3. def OAI.HadwigerCounterexample.obsZ line 28
4. theorem OAI.HadwigerCounterexample.obsZ_self line 40
5. theorem OAI.HadwigerCounterexample.two_eval line 47
6. theorem OAI.HadwigerCounterexample.obsZ_surj line 65
7. def OAI.HadwigerCounterexample.selfPartial line 87
8. theorem OAI.HadwigerCounterexample.pull_selfPart line 91
9. def OAI.HadwigerCounterexample.obsHalf line 101
10. theorem OAI.HadwigerCounterexample.obsHalf_surj line 119

    Source documentation

    Uniform off-diagonal block even in transpose-character case.

    theorem obsHalf_surj (s t : Label p.b) (hs : s≠t) {f : Vec Bool} (hf : f≠0) (n : ℕ)
        {l r : Fin (n/2)→Fin n} (hl : Function.Injective l) (hr : Function.Injective r)
        (h : ∀ i j,l i≠r j) : Function.Surjective (obsHalf p s t f n l r) := by
    …

    Mentions: OAI.HadwigerCounterexample.Label, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.obsHalf