OAI/Analysis/WeakInfiniteness/BoundedImplementation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.boundedCutFunction line 25
2. lemma OAI.WeakPureInfiniteness.continuous_boundedCutFunction line 27
3. lemma OAI.WeakPureInfiniteness.boundedCutFunction_zero line 35
4. lemma OAI.WeakPureInfiniteness.boundedCutFunction_mul line 38
5. lemma OAI.WeakPureInfiniteness.boundedCutFunction_square_le line 47
6. lemma OAI.WeakPureInfiniteness.boundedCutFunction_cfc_product line 60
7. lemma OAI.WeakPureInfiniteness.boundedCutFunction_cfc_norm line 77
8. lemma OAI.WeakPureInfiniteness.exists_bounded_cut_implementation line 119