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

eligible_mono

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)

 292lemma eligible_mono {picked₁ picked₂ : Finset E.Event}
 293    (hsubset : picked₁ ⊆ picked₂) {e : E.Event}
 294    (helig : eligible (ev:=ev) picked₁ e) :

proof body

Tactic-mode proof.

 295    eligible (ev:=ev) picked₂ e := by
 296  intro v hv
 297  exact hsubset (helig hv)
 298

depends on (2)

Lean names referenced from this declaration's body.