OAI/Analysis/CircleDomains/Rigidity/MaskedTerminalLabel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A terminal inside a physical mask has its original quotient label in that mask. Nonempty label fibers are supplied by the component quotient.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.label_mem_mask_of_terminal_inside line 13