OAI/Analysis/CircleDomains/Modulus/FlexibleCirclePayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Line payment is independent of which endpoint carries the value zero.

  1. theorem OAI.CircleDomainRigidity.line_payment_through_disks_one_zero line 14
  2. theorem OAI.CircleDomainRigidity.parallel_line_payment_in_region_either_order line 45