eligible_mono

formal source

 289def eligible (picked : Finset E.Event) (e : E.Event) : Prop :=
 290  ∀ {v}, Prec v e → v ∈ picked
 291
 292lemma eligible_mono {picked₁ picked₂ : Finset E.Event}
 293    (hsubset : picked₁ ⊆ picked₂) {e : E.Event}
 294    (helig : eligible (ev:=ev) picked₁ e) :
 295    eligible (ev:=ev) picked₂ e := by
 296  intro v hv
 297  exact hsubset (helig hv)
 298
 299lemma exists_minimal_eligible (picked : Finset E.Event)
 300    (h : ∃ e, e ∉ picked) :
 301    ∃ e, e ∉ picked ∧ eligible (ev:=ev) picked e := by
 302  classical
 303  have wf := ledger_prec_wf (ev:=ev)
 304  let S : Set E.Event := {x | x ∉ picked}
 305  have hS : S.Nonempty := by
 306    rcases h with ⟨e, he⟩
 307    exact ⟨e, he⟩
 308  obtain ⟨m, hmS, hmin⟩ := wf.has_min S hS
 309  refine ⟨m, hmS, ?_⟩
 310  intro v hv
 311  by_contra hvPicked
 312  have hvS : v ∈ S := hvPicked
 313  exact (hmin v hvS hv)
 314
 315structure Candidate (picked : Finset E.Event) where
 316  idx : ℕ
 317  event : E.Event
 318  event_def : enum (E:=E) idx = event
 319  not_mem : event ∉ picked
 320  eligible_event : eligible (ev:=ev) picked event
 321
 322lemma exists_candidate_index (picked : Finset E.Event)