OAI/Computability/VertexCover/Reduction/ConditionNested.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Restriction.EnergyForm.finite line 44
  2. theorem OAI.VertexCover.Restriction.EnergyForm.finite_form line 63
  3. theorem OAI.VertexCover.Restriction.EnergyForm.finite_energy line 66
  4. def OAI.VertexCover.Restriction.EnergyForm.Projection.lift line 72
  5. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.lift_apply line 83
  6. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_lift line 86
  7. def OAI.VertexCover.Restriction.EnergyForm.Projection.fiberSize line 96
  8. def OAI.VertexCover.Restriction.EnergyForm.Projection.fiberKernel line 100
  9. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.fiberSize_pos line 104
  10. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.fiberKernel_symm line 108
  11. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.fiberKernel_sum line 114
  12. def OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap line 121
  13. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_apply line 130
  14. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_congr line 133
  15. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_eq_of_key_eq line 148
  16. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_of_invariant line 155
  17. def OAI.VertexCover.Restriction.EnergyForm.Projection.condition line 167
  18. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.condition_apply line 182
  19. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.condition_lift_commute line 185
  20. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.condition_nested line 191