OAI/Analysis/CircleDomains/Modulus/TupleIncidence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Incidence of a tuple with a fixed dust point. A free point whose individual level sections are null has a null incident-tuple set.

  1. def OAI.CircleDomainRigidity.tupleIncident line 17
  2. theorem OAI.CircleDomainRigidity.isClosed_tupleIncident line 20
  3. theorem OAI.CircleDomainRigidity.tupleIncident_fiber_null line 38
  4. theorem OAI.CircleDomainRigidity.tupleReference_incident_null line 52