OAI/Analysis/CircleDomains/Topology/MixedCircleFillings.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous real and circle fillings using the same rank-one collar extensions. Exact real values are retained for the designated real coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_exists_mixed_filled_coordinates line 14
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_fill_actual_mixed_cutoff line 140