OAI/Analysis/CircleDomains/Selection/DiffuseDustIntersections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removal of diffuse dust intersections from the actual residual constraints, tuple laws, and ordered compatibility of the coordinate list.

  1. theorem OAI.CircleDomainRigidity.tag_interval_of_not_residual line 16

    Also declared: OAI/Analysis/CircleDomains/Selection/DustBoundDiffuseIntersections.lean:16 (same declaration text), OAI/Analysis/CircleDomains/Selection/RankedDiffuseIntersections.lean:16 (same declaration text).

  2. theorem OAI.CircleDomainRigidity.ae_diffuse_dust_intersections line 34