OAI/Analysis/CircleDomains/Transfer/ModelLocalizedSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous selection may keep every changed support in a prescribed source disk containing the dust. This leaves the outer working collar unchanged.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_flattened_source_selection_in_ball line 15