OAI/Analysis/WeakInfiniteness/CuntzComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.CuntzSubequiv line 17

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:138 (same declaration text).

2. def OAI.WeakPureInfiniteness.blockSum line 20

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:141 (same declaration text).

3. def OAI.WeakPureInfiniteness.ProperlyInfinite line 25

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:146 (same declaration text).

4. def OAI.WeakPureInfiniteness.diagonalCopies line 28

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:149 (same declaration text).

5. def OAI.WeakPureInfiniteness.WeaklyPurelyInfinite line 33

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:154 (same declaration text).

6. def OAI.WeakPureInfiniteness.StronglyPurelyInfinite line 36

   Also declared: ComparatorChallenges/ExactInfiniteness.lean:157 (same declaration text).