OAI/Analysis/CircleDomains/Selection/FullDomainPhysicalLift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An arbitrary finite physical path wholly in the quotient domain has an actual rectifiable physical lift with exactly the original occupation.

  1. def OAI.CircleDomainRigidity.fullDomainPhysicalLift line 20
  2. theorem OAI.CircleDomainRigidity.fullDomainPhysicalLift_mem line 29
  3. theorem OAI.CircleDomainRigidity.fullDomainPhysicalLift_value line 37
  4. theorem OAI.CircleDomainRigidity.fullDomainPhysicalLift_project line 45
  5. theorem OAI.CircleDomainRigidity.fullDomainPhysicalLift_projects line 58
  6. theorem OAI.CircleDomainRigidity.dyadicPhysicalOccupation_fullDomainLift line 69