OAI/SetTheory/PartitionPrinciple/Forcing/ActiveNameImageSymmetry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.activeImage line 12
  2. theorem OAI.PartitionPilot.Forcing.Name.entry_activeImage line 19
  3. theorem OAI.PartitionPilot.Forcing.Name.activeImage_subset line 31
  4. theorem OAI.PartitionPilot.Forcing.Name.activeImage_congr line 40
  5. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_activeImage line 53
  6. theorem OAI.PartitionPilot.Forcing.Name.act_activeImage line 81
  7. theorem OAI.PartitionPilot.Forcing.Name.activeImage_support line 109
  8. theorem OAI.PartitionPilot.Forcing.Name.activeImage_hs line 120
  9. def OAI.PartitionPilot.Forcing.SetFormula.activeNameImageEntryFormula line 145
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_activeNameImageEntryFormula line 163
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.activeImage_eq_selection line 218
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.activeImage_mem line 248