OAI/Analysis/CircleDomains/Topology/MontelCutoffExhaustion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported cutoffs for a varying open exhaustion. The chosen subsequence is increasing and each fixed compact set eventually lies in the region on which its cutoff is exactly one.

  1. theorem OAI.CircleDomainRigidity.exists_montel_exhaustion_cutoffs line 15