OAI/Analysis/CircleDomains/Selection/ScalarEndCaps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual matched source caps shrink to their complementary component. Continuous component-constant tests therefore have arbitrarily small ranges on all sufficiently late caps.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.eventually_source_cap_subset line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.eventually_source_values line 29