OAI/SetTheory/PartitionPrinciple/Definability/VisibilityProfileFormulas.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.stageOneRawProfile line 11
  2. def OAI.PartitionPilot.Forcing.stageOneRawCompatibility line 16
  3. def OAI.PartitionPilot.Forcing.SetFormula.stageOneProfileAt line 22
  4. def OAI.PartitionPilot.Forcing.SetFormula.stageOneCompatibilityAt line 29
  5. theorem OAI.PartitionPilot.Forcing.map_three line 37

    Also declared: OAI/SetTheory/PartitionPrinciple/Definability/GroundPackedRefinementFormulaData.lean:56 (same declaration text).

  6. theorem OAI.PartitionPilot.Forcing.map_four line 42

    Also declared: OAI/SetTheory/PartitionPrinciple/Definability/GroundPackedRefinementFormulaData.lean:157 (same declaration text).

  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOnePairLookup line 50
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneProfileAt line 56
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_stageOneCompatibilityAt line 89
  10. def OAI.PartitionPilot.Forcing.SetFormula.supportedEqualitySequenceFormula line 122
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_supportedEqualitySequenceFormula line 133
  12. def OAI.PartitionPilot.Forcing.SetFormula.visibilityProfileFormula line 172
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_visibilityProfileFormula line 180