OAI/SetTheory/PartitionPrinciple/Definability/RawCheckFormulas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.Name.mem_check_code line 12
2. def OAI.PartitionPilot.Forcing.SetFormula.checkStepFormula line 27
3. def OAI.PartitionPilot.Forcing.TransitiveGround.RawCheckStep line 43
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawCheckStep_mono line 47
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_checkStepFormula line 57
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rawCheckStep_eq line 106