OAI/Analysis/CircleDomains/Probability/LocalNullImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local null-image criterion

Restrict the connected-neighborhood oscillation argument to an open region. Oscillation need only be controlled on connected open sets inside that region; no behavior across its boundary is required.

  1. theorem OAI.CircleDomainRigidity.null_image_inter_open_of_connected_open_oscillation line 17