OAI/SetTheory/PartitionPrinciple/Geometry/CompleteProjectionPredensity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.CompleteProjection line 12
  2. theorem OAI.PartitionPilot.Forcing.CompleteProjection.le_include_restriction line 23
  3. theorem OAI.PartitionPilot.Forcing.CompleteProjection.compatible_include_iff line 26
  4. theorem OAI.PartitionPilot.Forcing.CompleteProjection.included_compatible_iff line 36
  5. theorem OAI.PartitionPilot.Forcing.CompleteProjection.dense_preimage line 40
  6. theorem OAI.PartitionPilot.Forcing.CompleteProjection.predense_inclusion line 50
  7. def OAI.PartitionPilot.Forcing.CompleteProjection.projectedFilter line 57
  8. theorem OAI.PartitionPilot.Forcing.CompleteProjection.projectedFilter_mem_iff line 71
  9. theorem OAI.PartitionPilot.Forcing.CompleteProjection.projectedFilter_meets_iff line 80
  10. theorem OAI.PartitionPilot.Forcing.CompleteProjection.projectedFilter_generic line 90
  11. theorem OAI.PartitionPilot.Forcing.CompleteProjection.denseBelow_preimage_iff line 109
  12. theorem OAI.PartitionPilot.Forcing.Name.forcesEq_rename_completeProjection line 133
  13. theorem OAI.PartitionPilot.Forcing.Name.memWitness_rename_completeProjection line 190
  14. theorem OAI.PartitionPilot.Forcing.Name.forcesMem_rename_completeProjection line 203
  15. theorem OAI.PartitionPilot.Forcing.CompleteProjection.predense_inclusion_iff line 226
  16. theorem OAI.PartitionPilot.Forcing.CompleteProjection.raw_predense_restriction line 235