OAI/SetTheory/PartitionPrinciple/Forcing/RefinementCoarseImageNames.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.coarseClassImage line 12
  2. theorem OAI.PartitionPilot.Forcing.mem_coarseClassImage line 15
  3. theorem OAI.PartitionPilot.Forcing.coarseClassImage_of_fineClass line 19
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.coarseClassImageFormula line 34
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_coarseClassImageFormula line 37
  6. def OAI.PartitionPilot.Forcing.Name.refinementCoarseImage line 50
  7. theorem OAI.PartitionPilot.Forcing.Name.entry_refinementCoarseImage line 55
  8. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementCoarseImage line 68
  9. theorem OAI.PartitionPilot.Forcing.Name.eval_refinementCoarseImage_of_subset line 97
  10. theorem OAI.PartitionPilot.Forcing.Name.refinementCoarseImage_support line 113