ModelPriorityData.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual countable ends, selected target points and a common horizontal bound for priority interpolation. The enumeration may repeat a harmless point end when the nonpoint family is finite or empty.

theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_priority_source_data line 16