OAI/Analysis/CircleDomains/Selection/TerminalContainment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retained cores localize every marked terminal

A connected terminal disk disjoint from a retained core lies in one of that core's holes. A point of the terminal identifies which hole it is. Thus retaining the core and retaining a mark already imply the physical containment needed for the target trapping argument.

  1. theorem OAI.CircleDomainRigidity.terminal_subset_retained_side line 23