OAI/Analysis/CircleDomains/Selection/VerticalRealRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual retained real tests give vertical target crossing segments.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_vertical_test_crossings line 16