OAI/Analysis/CircleDomains/Transfer/MixedCoordinateModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual common model for both real barriers and masked periods. Real terminal bounds include every mark.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.nonempty_mixed_coordinate_stage line 18