OAI/SetTheory/PartitionPrinciple/Definability/StrictLexHeightFormulas.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.strictLexHeightFormula line 12
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_strictLexHeightFormula line 23
3. def OAI.PartitionPilot.Forcing.BoundedFormula.heightColumnsBoundFormula line 43
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightColumnsBoundFormula line 48
5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_heightColumnsBoundFormula_of_function line 56
6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_strictLexHeightFormula line 70
7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_heightColumnsBoundFormula line 77