'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]
'UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletGlue.glue_bare_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletGlue.glue_observable' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletGlue.glue_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
