OAI/Analysis/CircleDomains/Selection/ResidualTagAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Independent later tags avoid the scalar-level null envelopes of an earlier residual image. The product event is built from Borel envelopes.

  1. theorem OAI.CircleDomainRigidity.ae_product_no_bad_tag_level line 18