pith. machine review for the scientific record. sign in
structure definition def or abbrev

DirectedRefinement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  57structure DirectedRefinement (C : Type*) where
  58  EventType : ℕ → Type*
  59  recognizer : (i : ℕ) → Recognizer C (EventType i)
  60  refines : ∀ i : ℕ, IsFinerThan' (recognizer (i + 1)) (recognizer i)
  61
  62/-- The refinement is monotone: later recognizers are always finer. -/
  63theorem DirectedRefinement.monotone_refines (sys : DirectedRefinement C)
  64    {i j : ℕ} (hij : i ≤ j) :
  65    IsFinerThan' (sys.recognizer j) (sys.recognizer i) := by

proof body

Definition body.

  66  induction hij with
  67  | refl => exact isFinerThan'_refl _
  68  | step _ ih =>
  69    exact isFinerThan'_trans _ _ _ (sys.refines _) ih
  70
  71/-- U2: The convergence condition for a directed refinement system.
  72The refinement eventually separates any two distinguishable points:
  73for any c₁ ≠ c₂ in C, there exists an index i such that R_i
  74distinguishes them. -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.