OAI/SetTheory/PartitionPrinciple/Definability/GroundSemanticOrdinalRowOrbitCovers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.acted_pair line 18
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitPairGraph_code_eq line 24
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitPairGraph_ground_hs line 62
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTuple_equal_relativeFix line 112
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.liftedRowOrbit_function line 145
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_rowProjection line 273
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticBinaryRow_orbit_function line 342
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticBinaryRow_orbit_cover line 491
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticBinaryRow_ordinal_partial_cover line 796