OAI/Analysis/CircleDomains/Selection/MixedRealStage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real part of a mixed model satisfies the existing real-stage interface. Its map and metric are the same ones used by its period tests.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.ModelRealSubfamily.realTransferStage line 15