OAI/Analysis/CircleDomains/Selection/IndependentTagLevel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute continuity of tag tuples supplies the independent-level singleton conclusion for almost every path and almost every level.

  1. theorem OAI.CircleDomainRigidity.tupleReference_product_right_null line 15
  2. theorem OAI.CircleDomainRigidity.tupleReference_single_level_incompatible_null line 32
  3. def OAI.CircleDomainRigidity.activeSlotParameterEvent line 59
  4. theorem OAI.CircleDomainRigidity.measurableSet_activeSlotParameterEvent line 63
  5. theorem OAI.CircleDomainRigidity.ae_active_slots_avoid_independent_null line 83
  6. theorem OAI.CircleDomainRigidity.ae_tag_contacts_singleton_at_independent_level line 122