pith. machine review for the scientific record. sign in
lemma proved wrapper

InCover_of_mem

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  45@[simp] lemma InCover_of_mem {S : List Nat} {v : Nat} (h : v ∈ S) : InCover S v := by

proof body

One-line wrapper that applies simpa.

  46  simpa [InCover] using h
  47

depends on (2)

Lean names referenced from this declaration's body.