isRecognitionConnected_singleton

formal source

  51  exact absurd h₁ (Set.not_mem_empty c₁)
  52
  53/-- A singleton set is recognition-connected -/
  54theorem isRecognitionConnected_singleton (r : Recognizer C E) (c : C) :
  55    IsRecognitionConnected r {c} := by
  56  intro c₁ c₂ h₁ h₂
  57  simp only [Set.mem_singleton_iff] at h₁ h₂
  58  rw [h₁, h₂]
  59  exact Indistinguishable.refl r c
  60
  61/-- A resolution cell is recognition-connected by definition -/
  62theorem isRecognitionConnected_resolutionCell (r : Recognizer C E) (c : C) :
  63    IsRecognitionConnected r (ResolutionCell r c) := by
  64  intro c₁ c₂ h₁ h₂
  65  simp only [ResolutionCell, Set.mem_setOf_eq] at h₁ h₂
  66  exact Indistinguishable.trans r h₁ (Indistinguishable.symm' r h₂)
  67
  68/-- A subset of a recognition-connected set is recognition-connected -/
  69theorem isRecognitionConnected_subset (r : Recognizer C E) {S T : Set C}
  70    (hST : S ⊆ T) (hT : IsRecognitionConnected r T) :
  71    IsRecognitionConnected r S := by
  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. -/
  82def IsLocallyRegular (L : LocalConfigSpace C) (r : Recognizer C E) (c : C) : Prop :=
  83  ∃ U ∈ L.N c, IsRecognitionConnected r (r.R ⁻¹' {r.R c} ∩ U)
  84