OAI/SetTheory/PartitionPrinciple/Forcing/IdealChain.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain line 11
  2. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.up line 19
  3. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.up_self line 22
  4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.up_succ line 25
  5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.up_comp line 29
  6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.up_le line 33
  7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.up_ideal line 39
  8. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.raise line 49
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.Label line 52
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.Related line 54
  11. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.related_refl line 57
  12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.related_symm line 59
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.related_trans line 63
  14. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.setoid line 76
  15. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.Union line 77
  16. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.point line 78
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.include_up line 80
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.include_injective line 85
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.cover line 90
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.pair_cover line 94
  21. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.Le line 101
  22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.le_stage line 104
  23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.le_refl line 123
  24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.le_trans line 127
  25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.le_antisymm line 139
  26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.include_ideal line 144
  27. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.stage_meet_spec line 155
  28. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.meets_exist line 167
  29. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.unionOrder line 172
  30. def OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.inclusion line 182
  31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.IdealChain.vertex_preserved line 185