OAI/Analysis/WeakInfiniteness/CompatibleSeparation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.UniformPerturbationOne_any line 34
2. lemma OAI.WeakPureInfiniteness.exists_uniformPerturbationOne_any line 44
3. lemma OAI.WeakPureInfiniteness.metric_column_expansion_any line 56
4. lemma OAI.WeakPureInfiniteness.metric_column_update_any line 65
5. lemma OAI.WeakPureInfiniteness.inr_snd_mul_inr_any line 81
6. lemma OAI.WeakPureInfiniteness.exists_compatible_metric_perturbations_any line 86