OAI/SetTheory/PartitionPrinciple/Forcing/GroundProjectedRowChooserWitnesses.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.symmetricExtension line 17
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_symmetricExtension line 21
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.symmetricExtension_subset_ordinaryExtension line 27
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ground_subset_symmetricExtension line 33
5. def OAI.PartitionPilot.Forcing.Name.supportedFamilyCodes line 57
6. theorem OAI.PartitionPilot.Forcing.Name.mem_supportedFamilyCodes line 60
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedFamilyCodes_mem line 78
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.supportedNameSequence_function_mem line 126
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundOrdinalFixedNameSequence line 166
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.liftedInternalRowSet_mem line 250
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.liftedInternalRows_chooser_witness line 273