OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalAlphabetInversion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.externalSymbolInverse line 12
2. theorem OAI.PartitionPilot.Forcing.externalSymbolInverse_involutive line 16
3. def OAI.PartitionPilot.Forcing.ExternalSymbolInverseEntry line 23
4. def OAI.PartitionPilot.Forcing.externalSymbolInverseGraph line 28
5. theorem OAI.PartitionPilot.Forcing.pair_mem_externalSymbolInverseGraph line 34
6. theorem OAI.PartitionPilot.Forcing.externalSymbolInverseGraph_eq_graph line 51
7. theorem OAI.PartitionPilot.Forcing.externalSymbolInverseGraph_entry_iff line 79
8. theorem OAI.PartitionPilot.Forcing.externalSymbolInverseGraph_function line 87
9. def OAI.PartitionPilot.Forcing.BoundedFormula.externalSymbolInverseFormula line 106
10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalSymbolInverseFormula line 118
11. def OAI.PartitionPilot.Forcing.BoundedFormula.externalSymbolInverseEntryFormula line 143
12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalSymbolInverseEntryFormula line 150
13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalSymbolInverseGraph_mem line 175