OAI/Computability/VertexCover/Reduction/NormAttainedSupport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.LabelCover.compatibleSelections line 40
  2. theorem OAI.VertexCover.LabelCover.mem_compatibleSelections line 45
  3. theorem OAI.VertexCover.LabelCover.compatible_empty line 50
  4. theorem OAI.VertexCover.LabelCover.compatibleSelections_nonempty line 54
  5. def OAI.VertexCover.LabelCover.compatibilityNorm line 58
  6. theorem OAI.VertexCover.LabelCover.form_le_norm line 63
  7. theorem OAI.VertexCover.LabelCover.norm_le_iff line 69
  8. theorem OAI.VertexCover.LabelCover.norm_nonneg line 77
  9. theorem OAI.VertexCover.LabelCover.norm_zero line 81
  10. theorem OAI.VertexCover.LabelCover.coordinate_le_norm line 87
  11. theorem OAI.VertexCover.LabelCover.norm_eq_zero_iff line 92
  12. theorem OAI.VertexCover.LabelCover.norm_add_le line 103
  13. theorem OAI.VertexCover.LabelCover.norm_mul line 114
  14. theorem OAI.VertexCover.LabelCover.norm_neg line 128
  15. theorem OAI.VertexCover.LabelCover.norm_attained_on_support line 133