OAI/Analysis/SeparableQuotients/ExactPairs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.ActualSpace.exists_finite_vector_normer line 11
2. lemma OAI.SeparableQuotient.ActualSpace.vectorCrop_mono line 42
3. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.support_subset_sum line 58
4. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.sum_nonzero line 73
5. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.normer_cross line 80
6. structure OAI.SeparableQuotient.ActualSpace.ExactPair line 93

   Source documentation

   Exact pairs with uncropped child legality and support bounds in both orders.

   structure ExactPair {f : Family} (z : BlockSequence f) (a J : ℕ) where
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence

7. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.exists_exactPair line 105