OAI/Analysis/CircleDomains/Topology/CircleAlmostEverywhere.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere assertions on the unit circle from their real representatives. No measurability of the asserted property is required.

  1. theorem OAI.CircleDomainRigidity.ae_real_interval_of_ae_circle line 12
  2. theorem OAI.CircleDomainRigidity.ae_circle_of_ae_unit_interval line 17