OAI/SetTheory/PartitionPrinciple/Forcing/PairFamilyEvaluation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.orderedPairNameFamily_valid line 13
  2. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamily_valid line 22
  3. theorem OAI.PartitionPilot.Forcing.orderedPairNameFamily_hs line 32
  4. theorem OAI.PartitionPilot.Forcing.orderedPairNameFamily_closed line 47
  5. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamily_hs line 68
  6. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamily_closed line 79
  7. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamilySet_invariant line 90
  8. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamilySet_hs line 100
  9. theorem OAI.PartitionPilot.Forcing.Name.eval_familySet_orderedPairNameFamily line 119
  10. theorem OAI.PartitionPilot.Forcing.Name.refinementValidity_familySet_power_bounds line 148