OAI/Analysis/CircleDomains/Transfer/EnlargedRealModels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Enlarge the common exterior radius without changing the actual finite models or their transferred coordinates.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.withRadius line 18
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_real_model_exhaustion_large_radius line 45