377lemma minIndex_min (e : E.Event) {n : ℕ} (h : enum (E:=E) n = e) :
proof body
Tactic-mode proof.
378 minIndex (E:=E) e ≤ n := by 379 classical 380 unfold minIndex 381 exact Nat.find_min' (enum_surjective (E:=E) e) h 382 383/-- A canonical countable schedule derived from `minIndex`. Each event appears 384 exactly once at its minimal enumeration index. -/
depends on (11)
Lean names referenced from this declaration's body.