resolutionCell_eq_iff

formal source

  82  simp [ResolutionCell, Indistinguishable, Recognizer.fiber]
  83
  84/-- Two configurations have the same resolution cell iff they're indistinguishable -/
  85theorem resolutionCell_eq_iff {c₁ c₂ : C} :
  86    ResolutionCell r c₁ = ResolutionCell r c₂ ↔ c₁ ~[r] c₂ := by
  87  constructor
  88  · intro h
  89    have : c₂ ∈ ResolutionCell r c₁ := by
  90      rw [h]
  91      exact mem_resolutionCell_self r c₂
  92    exact (Indistinguishable.symm' r this)
  93  · intro h
  94    ext c
  95    simp [ResolutionCell, Indistinguishable]
  96    constructor
  97    · intro hc
  98      exact Eq.trans hc h
  99    · intro hc
 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) :=