`Covers_nil_edges`

proved

show as: view math explainer →

module: IndisputableMonolith.Complexity.VertexCover
domain: Complexity
line: 52 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.VertexCover on GitHub at line 52.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.