finite_resolution_event_in_finite

formal source

  44variable (L : LocalConfigSpace C) (r : Recognizer C E)
  45
  46/-- If R has finite local resolution at c, then c's event is in a finite set -/
  47theorem finite_resolution_event_in_finite (c : C)
  48    (h : HasFiniteLocalResolution L r c) :
  49    ∃ S : Set E, S.Finite ∧ r.R c ∈ S := by
  50  obtain ⟨U, hU, hfin⟩ := h
  51  exact ⟨r.R '' U, hfin, ⟨c, L.mem_of_mem_N c U hU, rfl⟩⟩
  52
  53/-- Finite resolution is inherited by smaller neighborhoods -/
  54theorem finite_resolution_mono {c : C} {U V : Set C}
  55    (hU : U ∈ L.N c) (hV : V ∈ L.N c) (hVU : V ⊆ U) (hfin : (r.R '' U).Finite) :
  56    (r.R '' V).Finite :=
  57  Set.Finite.subset hfin (Set.image_mono hVU)
  58
  59/-! ## Consequences for Resolution Cells -/
  60
  61/-- If R has finite local resolution at c, the resolution cell at c
  62    has a finite number of "neighbors" in any finite-resolution neighborhood -/
  63theorem finite_resolution_cell_finite_events (c : C)
  64    (h : HasFiniteLocalResolution L r c) :
  65    ∃ U ∈ L.N c, ∀ c' ∈ U, r.R c' ∈ r.R '' U ∧ (r.R '' U).Finite := by
  66  obtain ⟨U, hU, hfin⟩ := h
  67  use U, hU
  68  intro c' hc'
  69  exact ⟨⟨c', hc', rfl⟩, hfin⟩
  70
  71/-! ## Discrete Local Recognition Geometry -/
  72
  73/-- A recognition geometry is locally discrete if events are finite everywhere -/
  74def IsLocallyDiscrete (L : LocalConfigSpace C) (r : Recognizer C E) : Prop :=
  75  HasFiniteResolution L r
  76
  77/-- In a locally discrete recognition geometry, every neighborhood contains