pith. machine review for the scientific record. sign in
theorem proved term proof

quotientMk_respects_event

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  44theorem quotientMk_respects_event {c₁ c₂ : C}
  45    (h : recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂) :
  46    r.R c₁ = r.R c₂ :=

proof body

Term-mode proof.

  47  (quotientMk_eq_iff r).mp h
  48
  49/-- The quotient is nonempty if C is -/
  50instance [ConfigSpace C] : Nonempty (RecognitionQuotient r) :=
  51  ⟨recognitionQuotientMk r (ConfigSpace.witness C)⟩
  52
  53/-! ## Event Map on Quotient -/
  54
  55/-- The event map factors through the quotient: R = R̄ ∘ π -/

depends on (12)

Lean names referenced from this declaration's body.