OAI/Analysis/CircleDomains/Probability/MarkedFusionKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing all basis neighborhoods whose intersection with a closed candidate set is test-small leaves a closed nonsmall kernel. Every neighborhood of every remaining point meets the kernel nonsmally, as needed by the finite fusion split.

  1. theorem OAI.CircleDomainRigidity.MarkedHit.exists_closed_hit_test_kernel line 23