OAI/Analysis/CircleDomains/Probability/MeasurableTerminalArcs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Apply the published measurable selection theorem to the actual Borel relation of simple subarcs of the last-entry terminal path.

  1. theorem OAI.CircleDomainRigidity.exists_measurable_terminal_arc_selector line 20
  2. theorem OAI.CircleDomainRigidity.terminal_arc_selector_properties line 59