OAI/SetTheory/PartitionPrinciple/Geometry/GroundLinkedProfilePreservation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.retargetLinked_preservesOldProfiles_iff line 14
2. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.preservesOldProfiles_iff_of_map_code line 27
3. def OAI.PartitionPilot.Forcing.LinkedProfilePreservingTransitionCode line 37
4. theorem OAI.PartitionPilot.Forcing.LinkedProfilePreservingTransitionCode.linked_transition line 47
5. theorem OAI.PartitionPilot.Forcing.LinkedProfilePreservingTransitionCode.exists_at line 52
6. theorem OAI.PartitionPilot.Forcing.LinkedProfilePreservingTransitionCode.preserves_at line 62