OAI/Analysis/CircleDomains/Probability/HeightHorizontalNullPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed conductivity height and the ordinary horizontal coordinate have a null-area joint trace on the omitted set.

  1. theorem OAI.CircleDomainRigidity.ControlledHeight.horizontal_pair_null line 13