OAI/Analysis/CircleDomains/Probability/SimpleArcMeasurability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Borel simple-path and image-containment relations for the measurable terminal-arc selection used in the stream construction.

  1. def OAI.CircleDomainRigidity.pathsWithSeparatedCollision line 17
  2. theorem OAI.CircleDomainRigidity.isClosed_pathsWithSeparatedCollision line 20
  3. theorem OAI.CircleDomainRigidity.injective_path_iff_no_separated_collision line 40
  4. theorem OAI.CircleDomainRigidity.measurableSet_injective_paths line 56
  5. theorem OAI.CircleDomainRigidity.isClosed_path_image_containment line 66