OAI/Analysis/CircleDomains/Topology/TerminalJordanForward.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The converse collar incidence: a source terminal in the retained bounded side has its assigned target component in the target bounded side.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.target_inside_of_source_inside line 14