resolutionCell_eq_fiber

formal source

  76  Indistinguishable.refl r c
  77
  78/-- Resolution cells are exactly the fibers of the recognizer -/
  79theorem resolutionCell_eq_fiber (c : C) :
  80    ResolutionCell r c = r.fiber (r.R c) := by
  81  ext c'
  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