OAI/Analysis/CircleDomains/Modulus/RealBarrierCollapse.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Vanishing retained real barriers collapse compact target continua.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.real_projection_payment line 15
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.real_projection_zero_of_vanishing_barriers line 40
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.subsingleton_of_vanishing_barriers line 85