pith. machine review for the scientific record. sign in
theorem proved term proof

isRecognitionConnected_subset

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)

  69theorem isRecognitionConnected_subset (r : Recognizer C E) {S T : Set C}
  70    (hST : S ⊆ T) (hT : IsRecognitionConnected r T) :
  71    IsRecognitionConnected r S := by

proof body

Term-mode proof.

  72  intro c₁ c₂ h₁ h₂
  73  exact hT c₁ c₂ (hST h₁) (hST h₂)
  74
  75/-! ## Local Regularity (RG5) -/
  76
  77/-- A recognizer is locally regular at c if the preimage of r(c) is
  78    recognition-connected within some neighborhood of c.
  79
  80    This means: nearby configurations that produce the same event
  81    are actually "coherently" grouped together. -/

used by (1)

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

depends on (19)

Lean names referenced from this declaration's body.