'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
