OAI/Analysis/WeakInfiniteness/CrossUniverseUniformGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.norm_tensorCut_wordTensor_le_of_models_any line 38
2. structure OAI.WeakPureInfiniteness.ExactModelDataAny line 51
3. lemma OAI.WeakPureInfiniteness.fixed_kernel_universal_of_arbitrarily_good_models line 61
4. theorem OAI.WeakPureInfiniteness.exists_uniform_gap_any line 137