lemma proved tactic proof

`chooseCandidate_none_iff`

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

formal statement (Lean)

 348lemma chooseCandidate_none_iff (picked : Finset E.Event) :
 349    chooseCandidate (ev:=ev) (E:=E) picked = none ↔

Tactic-mode proof.

 350      ¬∃ e, e ∉ picked := by
 351  classical
 352  unfold chooseCandidate
 353  split_ifs with h
 354  · simp [h]
 355  · simp [h]
 356

Lean names referenced from this declaration's body.