MaskedLineNullImage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local inactivity of each finite prefix, vanishing active tails and actual line payments force the unmasked trace of a null set to be null.

theorem OAI.CircleDomainRigidity.null_image_of_masked_line_payments line 16