isSeparating_iff

formal source

  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
  73
  74/-! ## Two-Recognizer Separation -/
  75
  76/-- Two recognizers together separate if their composite distinguishes all configs. -/