OAI/Analysis/CircleDomains/Selection/VerticalRealSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vertical payment along cofinal subsequences of actual real models.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.limiting_vertical_line_payment line 19