OAI/Analysis/CircleDomains/Selection/ScalarTerminalRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual matched terminal contours propagate source scalar ranges to their entire closed target disks, including all complementary dust.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.imageScalar_lt_on_terminal line 21
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.terminal_frontier_subset_image line 42
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.le_on_terminal line 53
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.ge_on_terminal line 63