OAI/Analysis/CircleDomains/Selection/RelevelledSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Installing the preceding selected level graphs in a path code leaves coordinates, flags, physical weights, and compatibility unchanged.

  1. def OAI.CircleDomainRigidity.SelectableMaskedCoordinate.withLevels line 19
  2. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.withLevels_reverse line 30
  3. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.CompatibleWith.withLevels line 35
  4. theorem OAI.CircleDomainRigidity.SelectableMaskedCoordinate.withLevels_injective line 54