OAI/Analysis/CircleDomains/Selection/RealSequenceRetention.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Retention of actual tests and their crossing segments along model subsequences.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_core_contains line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_model_contains line 26
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_test_eq line 30
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_test_crossings line 42