OAI/Analysis/CircleDomains/Probability/NullPairFromLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fubini for the compact image of a pair of continuous coordinates.

  1. theorem OAI.CircleDomainRigidity.null_pair_image_of_null_level_images line 12
  2. theorem OAI.CircleDomainRigidity.sobolev_height_pair_null_image line 34