IsSeparating

formal source

  39
  40/-- A recognizer **separates** a configuration space if it distinguishes
  41    all configurations (i.e., is injective on C). -/
  42def IsSeparating (r : Recognizer C E) : Prop :=
  43  Function.Injective r.R
  44
  45/-- A recognizer separates iff no two distinct configs are indistinguishable. -/
  46theorem isSeparating_iff (r : Recognizer C E) :
  47    IsSeparating r ↔ ∀ c₁ c₂, Indistinguishable r c₁ c₂ → c₁ = c₂ := by
  48  rfl
  49
  50/-- If a recognizer separates, the quotient is isomorphic to C. -/
  51theorem separating_quotient_bijective (r : Recognizer C E) (h : IsSeparating r) :
  52    Function.Bijective (recognitionQuotientMk r) := by
  53  constructor
  54  · -- Injective
  55    intro c₁ c₂ heq
  56    have hindist : Indistinguishable r c₁ c₂ := (quotientMk_eq_iff r).mp heq
  57    exact h hindist
  58  · -- Surjective
  59    intro q
  60    obtain ⟨c, hc⟩ := Quotient.exists_rep q
  61    use c
  62    simp only [recognitionQuotientMk]
  63    exact hc
  64
  65/-- If a recognizer separates, every resolution cell is a singleton. -/
  66theorem separating_singleton_cells (r : Recognizer C E) (h : IsSeparating r) (c : C) :
  67    ResolutionCell r c = {c} := by
  68  ext x
  69  simp only [ResolutionCell, Set.mem_setOf_eq, Set.mem_singleton_iff]
  70  constructor
  71  · intro hx; exact h hx
  72  · intro hx; subst hx; rfl