OAI/Combinatorics/HadwigerCounterexample/SpanDeficits.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.colsum_bound line 14

   Source documentation

   Loss of rank from overlapping mode spans.

   private theorem colsum_bound (A B : Mat I J) :
       A.rank+B.rank ≤ (A+B).rank+dim (colSp A⊓colSp B : Submodule _ _)+
         dim (colSp Aᵀ ⊓ colSp Bᵀ : Submodule _ _) := by
   …

   Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.dim, OAI.HadwigerCounterexample.colSp

2. theorem OAI.HadwigerCounterexample.cdim_mono line 42
3. theorem OAI.HadwigerCounterexample.cdim_bot line 44
4. theorem OAI.HadwigerCounterexample.cdim_sup_inf line 49
5. def OAI.HadwigerCounterexample.tax line 54
6. theorem OAI.HadwigerCounterexample.tax_before line 56
7. theorem OAI.HadwigerCounterexample.tax_lost line 59
8. theorem OAI.HadwigerCounterexample.tax_antitone line 63
9. theorem OAI.HadwigerCounterexample.matter_pair line 70
10. def OAI.HadwigerCounterexample.chopped line 99
11. theorem OAI.HadwigerCounterexample.matter_erased line 102
12. theorem OAI.HadwigerCounterexample.cdim_chopped line 111
13. def OAI.HadwigerCounterexample.arrange line 119
14. theorem OAI.HadwigerCounterexample.epoch_charge line 121
15. theorem OAI.HadwigerCounterexample.epoch_erased line 147
16. theorem OAI.HadwigerCounterexample.epoch_eq_zero line 150