isRecognitionConnected_empty

formal source

  45  ∀ c₁ c₂, c₁ ∈ S → c₂ ∈ S → Indistinguishable r c₁ c₂
  46
  47/-- The empty set is vacuously recognition-connected -/
  48theorem isRecognitionConnected_empty (r : Recognizer C E) :
  49    IsRecognitionConnected r ∅ := by
  50  intro c₁ c₂ h₁ _
  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.