OAI/Analysis/CircleDomains/Modulus/WeightedAnnularCollars.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite-cost smooth collar around a connected compact set, avoiding an outer closed obstacle. Used to place joining levels between fixed gates.

  1. theorem OAI.CircleDomainRigidity.isClosed_diff_of_frontier_disjoint line 16

    Distinct definitions of this name: OAI/Analysis/CircleDomains/Topology/MergeDisks.lean:24 (different declaration text). Qualify references as OAI.CircleDomainRigidity.isClosed_diff_of_frontier_disjoint@path.

  2. theorem OAI.CircleDomainRigidity.exists_weighted_collar_around_compact line 31