RestrictedSelectedFamily.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reduce the selected family to one countable set of marks while retaining its ordered compatibility and its real seed. No physical coordinate, mask, or boundary graph changes in this reduction.

theorem OAI.CircleDomainRigidity.exists_restricted_selected_family line 19