OAI/Analysis/CircleDomains/Selection/RestrictedFlattenedSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Keep the large disk needed for the compact source cutoff and restrict the same selection to the smaller disk on which that cutoff equals one.

  1. def OAI.CircleDomainRigidity.CompactScalarModel.FlattenedSourceSelection.restrictWorking line 14