OAI/Analysis/WeakInfiniteness/CrossUniverseUniformModels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.FiniteContractionModelsAny line 27
2. lemma OAI.WeakPureInfiniteness.minimalMapLeft_wordTensor_any line 35
3. lemma OAI.WeakPureInfiniteness.norm_model_amplifiedPolynomial_le_any line 44
4. lemma OAI.WeakPureInfiniteness.norm_faithfulAmplifiedPolynomial_le_of_models_any line 68
5. lemma OAI.WeakPureInfiniteness.norm_wordTensor_le_of_models_any line 108