OAI/Analysis/CircleDomains/Transfer/ModelPriorityContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual priority horizontal coordinate is continuous on the full finite source plane. Nonpoint ends use a terminating cutoff, and singleton fibers use the closed projection and shrinking Euclidean supports.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.priority_horizontal_plane_continuous line 18