OAI/SetTheory/PartitionPrinciple/Transfinite/GroundCanonicalCompressionHistory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.RecursiveStateData.canonicalHistory line 15
2. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.pair_mem_canonicalHistory line 18
3. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.canonicalHistory_function line 23
4. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.canonicalHistory_eq_of_entries line 38
5. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonicalHistory_spec line 67
6. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonicalHistory_mem line 81
7. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.realize_compressionHistory_iff line 86