resolutionCells_partition

formal source

 100      exact Eq.trans hc (Eq.symm h)
 101
 102/-- Resolution cells partition the configuration space -/
 103theorem resolutionCells_partition (c : C) :
 104    ∃! cell : Set C, c ∈ cell ∧ cell = ResolutionCell r c := by
 105  use ResolutionCell r c
 106  constructor
 107  · exact ⟨mem_resolutionCell_self r c, rfl⟩
 108  · intro cell ⟨_, hcell⟩
 109    exact hcell
 110
 111/-! ## Local Resolution -/
 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 -/