`chooseCandidate`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.Atomicity
domain: Foundation
line: 332 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.Atomicity on GitHub at line 332.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 329  · simpa [hn]
 330  · simpa [hn] using helig
 331
 332noncomputable def chooseCandidate (picked : Finset E.Event) :
 333    Option (Candidate (ev:=ev) (E:=E) picked) :=
 334  if h : ∃ e, e ∉ picked then
 335    let hx := exists_candidate_index (ev:=ev) (E:=E) picked h
 336    let n := Nat.find hx
 337    let hn := Nat.find_spec hx
 338    let e := enum (E:=E) n
 339    some
 340      { idx := n
 341      , event := e
 342      , event_def := rfl
 343      , not_mem := hn.left
 344      , eligible_event := hn.right }
 345  else
 346    none
 347
 348lemma chooseCandidate_none_iff (picked : Finset E.Event) :
 349    chooseCandidate (ev:=ev) (E:=E) picked = none ↔
 350      ¬∃ e, e ∉ picked := by
 351  classical
 352  unfold chooseCandidate
 353  split_ifs with h
 354  · simp [h]
 355  · simp [h]
 356
 357lemma chooseCandidate_some_spec {picked : Finset E.Event}
 358    {c : Candidate (ev:=ev) (E:=E) picked}
 359    (h : chooseCandidate (ev:=ev) (E:=E) picked = some c) :
 360    c.not_mem ∧ eligible (ev:=ev) picked c.event := by
 361  classical
 362  unfold chooseCandidate at h

papers checked against this theorem

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