LocalResolution

formal source

 112
 113/-- The local resolution of R at c on U is the partition of U into
 114    intersections with resolution cells. -/
 115def LocalResolution {C E : Type*} (r : Recognizer C E) (U : Set C) : Set (Set C) :=
 116  {S : Set C | ∃ c ∈ U, S = U ∩ ResolutionCell r c}
 117
 118/-- Local resolution cells cover U -/
 119theorem localResolution_covers (U : Set C) :
 120    ⋃₀ LocalResolution r U = U := by
 121  ext c
 122  simp only [Set.mem_sUnion, LocalResolution, Set.mem_setOf_eq]
 123  constructor
 124  · intro ⟨S, ⟨c', hc'U, hS⟩, hcS⟩
 125    rw [hS] at hcS
 126    exact hcS.1
 127  · intro hcU
 128    refine ⟨U ∩ ResolutionCell r c, ⟨c, hcU, rfl⟩, ?_⟩
 129    exact ⟨hcU, mem_resolutionCell_self r c⟩
 130
 131/-! ## Distinguishability -/
 132
 133/-- Two configurations are distinguishable if they produce different events -/
 134def Distinguishable {C E : Type*} (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
 135  r.R c₁ ≠ r.R c₂
 136
 137/-- Distinguishability is the negation of indistinguishability -/
 138theorem distinguishable_iff_not_indistinguishable {c₁ c₂ : C} :
 139    Distinguishable r c₁ c₂ ↔ ¬(c₁ ~[r] c₂) := Iff.rfl
 140
 141/-- There exist distinguishable configurations (by nontriviality) -/
 142theorem exists_distinguishable :
 143    ∃ c₁ c₂ : C, Distinguishable r c₁ c₂ :=
 144  r.nontrivial
 145