OAI/Analysis/CircleDomains/Topology/LocalInterposedCollars.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Interpose weighted collars between successive pairs of prescribed collars. All joining levels miss every prescribed boundary.

  1. theorem OAI.CircleDomainRigidity.exists_interposed_weighted_collars_of_local_energy line 15