InCover_cons

formal source

  39  intro e he
  40  simpa using he
  41
  42@[simp] lemma InCover_cons {x : Nat} {xs : List Nat} : InCover (x :: xs) x := by
  43  simp [InCover]
  44
  45@[simp] lemma InCover_of_mem {S : List Nat} {v : Nat} (h : v ∈ S) : InCover S v := by
  46  simpa [InCover] using h
  47
  48lemma EdgeCovered_comm (S : List Nat) (u v : Nat) :
  49  EdgeCovered S (u, v) ↔ EdgeCovered S (v, u) := by
  50  simp [EdgeCovered, Or.comm]
  51
  52lemma Covers_nil_edges (S : List Nat) (I : Instance) (h_edges : I.edges = []) : Covers S I := by
  53  intro e he
  54  simpa [Covers, h_edges] using he
  55
  56lemma hasCover_of_nil_edges (I : Instance) (h_edges : I.edges = []) : HasCover I := by
  57  refine ⟨[], by simp, ?_⟩
  58  intro e he
  59  simpa [Covers, h_edges] using he
  60
  61end VertexCover
  62
  63end Complexity
  64
  65end IndisputableMonolith