OAI/Analysis/CircleDomains/Topology/ModelFlattenedNeighborhoods.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common open source neighborhoods are constructed for the flattened old tests and the actual descended height.

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