OAI/Analysis/CircleDomains/Selection/DustBoundDiffuseIntersections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Diffuse dust intersections using only the visit bounds on dust marks. No visit bound is required at the distinguished image of infinity.

  1. theorem OAI.CircleDomainRigidity.tag_interval_of_not_residual line 16

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

  2. theorem OAI.CircleDomainRigidity.ae_diffuse_dust_intersections_of_dust_bounds line 34