OAI/SetTheory/PartitionPrinciple/Definability/IndexedSubstructureCodes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.indexedSuborderGraph line 11
2. def OAI.PartitionPilot.Forcing.indexedSubmeetGraph line 16
3. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedSuborderGraph line 22
4. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedSubmeetGraph line 37
5. theorem OAI.PartitionPilot.Forcing.suborderFiber_pair_iff line 55
6. theorem OAI.PartitionPilot.Forcing.submeetFiber_triple_iff line 66
7. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedSuborderEntryFormula line 80
8. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedSubmeetEntryFormula line 87
9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedSuborderEntryFormula line 95
10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedSubmeetEntryFormula line 106