  38  nontrivial : ∃ c₁ c₂ : C, R c₁ ≠ R c₂
  39
  40/-- A local recognizer is a recognizer on a local configuration space -/
  41structure LocalRecognizer (C : Type*) (E : Type*) extends
  42    LocalConfigSpace C, Recognizer C E
  43
  44/-! ## Basic Properties -/
  45
  46variable {C E : Type*}
  47
  48/-- The image of a recognizer has at least 2 elements -/
  49theorem Recognizer.image_nontrivial (r : Recognizer C E) :
  50    ∃ e₁ e₂ : E, e₁ ∈ Set.range r.R ∧ e₂ ∈ Set.range r.R ∧ e₁ ≠ e₂ := by
  51  obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
  52  exact ⟨r.R c₁, r.R c₂, ⟨c₁, rfl⟩, ⟨c₂, rfl⟩, hne⟩
  53
  54/-- A trivial recognizer maps everything to the same event -/
  55def Recognizer.isTrivial (r : Recognizer C E) : Prop :=
  56  ∀ c₁ c₂ : C, r.R c₁ = r.R c₂
  57
  58/-- No recognizer is trivial (by definition) -/
  59theorem Recognizer.not_trivial (r : Recognizer C E) : ¬r.isTrivial := by
  60  intro h
  61  obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
  62  exact hne (h c₁ c₂)
  63
  64/-! ## Local Image -/
  65
  66/-- The local image of a recognizer on a neighborhood -/
  67def Recognizer.localImage (r : Recognizer C E) (U : Set C) : Set E :=
  68  r.R '' U
  69
  70/-- Local image is subset of full image -/
  71theorem Recognizer.localImage_subset_range (r : Recognizer C E) (U : Set C) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.