HarmonicCountableCompactness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous harmonic limits on countably many interior balls

All local limits use the same original subsequence. Full support identifies the continuous source representatives, so the Euclidean limits agree on every overlap.

theorem OAI.RegularPointCoordinates.harmonic_countable_value_limits line 20