 279
 280local notation:max "Prec" => Precedence ev
 281
 282noncomputable def enum : ℕ → E.Event :=
 283  Classical.choose (Countable.exists_surjective_nat (E.countable))
 284
 285lemma enum_surjective : Function.Surjective (enum (E:=E)) :=
 286  Classical.choose_spec (Countable.exists_surjective_nat (E.countable))
 287
 288/-- An event is eligible once all predecessors have been posted. -/
 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

papers checked against this theorem

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