OAI/Combinatorics/ThinTrees/Blocks.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrongThinTree.MSS.blockDiagonal_nonneg line 15
2. lemma OAI.StrongThinTree.MSS.blockDiagonal_mono line 28
3. lemma OAI.StrongThinTree.MSS.blockDiag_mono line 35
4. lemma OAI.StrongThinTree.MSS.blockDiag_sum line 42
5. def OAI.StrongThinTree.MSS.blockEmbed line 48
6. lemma OAI.StrongThinTree.MSS.blockEmbed_trace line 52
7. lemma OAI.StrongThinTree.MSS.blockEmbed_mean line 57
8. lemma OAI.StrongThinTree.MSS.blockEmbed_blockDiag line 65
9. lemma OAI.StrongThinTree.MSS.blockDiagonal_sum line 72