OAI/Analysis/CircleDomains/Selection/ResidualProductAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Borel envelopes allow Tonelli to remove diffuse residual contacts without assuming that an uncountable incidence projection is Borel.

  1. theorem OAI.CircleDomainRigidity.ae_no_residual_incidence_of_null_envelopes line 18