OAI/Analysis/WeakInfiniteness/ContinuousDeletion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.ContinuouslySupported line 30
2. lemma OAI.WeakPureInfiniteness.cfc_partition_sum line 33
3. lemma OAI.WeakPureInfiniteness.cfc_mul_eq_zero_of_small_supports line 44
4. lemma OAI.WeakPureInfiniteness.vanishes_on_separated_sets line 65
5. theorem OAI.WeakPureInfiniteness.exists_continuous_spectral_deletion line 83
6. lemma OAI.WeakPureInfiniteness.both_signs_in_image_of_partition_diagonals line 132