OAI/Analysis/CircleDomains/Transfer/MixedMarkedModels.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Original marked ends in the common mixed model. These constructions use the actual terminal fibers; no transport of dependent terminal types from the real subfamily is necessary.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.markIndex line 25
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_markIndex line 28
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.core_model line 31
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_sourceMark_captured line 42
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_marked_cap_subset line 57
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_marked_cap_in_nhds line 69