OAI/Analysis/CircleDomains/Probability/OpenLineImageMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Countable open intervals convert local variation payment into a measure bound for the entire image, without requiring image measurability.

  1. theorem OAI.CircleDomainRigidity.open_line_image_measure_le line 12