finite_resolution_mono

formal source

  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
  78    only finitely many distinguishable configurations -/
  79theorem locally_discrete_finite_classes
  80    (h : IsLocallyDiscrete L r) (c : C) :
  81    ∃ U ∈ L.N c, (r.R '' U).Finite :=
  82  h c
  83
  84/-! ## No Continuous Injection Theorem -/