`chooseCandidate_none_iff`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.Atomicity on GitHub at line 348.

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

 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
 363  split_ifs at h with hExists
 364  · rcases h with ⟨⟩
 365    simp
 366  · cases h
 367
 368/-- Minimal index (in the fixed enumeration `enum`) where an event appears. -/
 369noncomputable def minIndex (e : E.Event) : ℕ :=
 370  Nat.find (enum_surjective (E:=E) e)
 371
 372lemma minIndex_spec (e : E.Event) : enum (E:=E) (minIndex (E:=E) e) = e := by
 373  classical
 374  unfold minIndex
 375  exact Nat.find_spec (enum_surjective (E:=E) e)
 376
 377lemma minIndex_min (e : E.Event) {n : ℕ} (h : enum (E:=E) n = e) :
 378    minIndex (E:=E) e ≤ n := by

papers checked against this theorem

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