separating_quotient_bijective

formal source

  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. -/
  77def PairSeparates {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
  78    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
  79  IsSeparating (r₁ ⊗ r₂)
  80
  81/-- Pair separation is equivalent to: same (e₁, e₂) implies same config. -/