`hasCover_of_nil_edges`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.VertexCover on GitHub at line 56.

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

  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.