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

pairSeparates_iff

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)

  82theorem pairSeparates_iff {E₁ E₂ : Type*} [EventSpace E₁] [EventSpace E₂]
  83    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  84    PairSeparates r₁ r₂ ↔
  85      ∀ c₁ c₂, (r₁.R c₁ = r₁.R c₂ ∧ r₂.R c₁ = r₂.R c₂) → c₁ = c₂ := by

proof body

Term-mode proof.

  86  simp only [PairSeparates, IsSeparating, Function.Injective, composite_R_eq,
  87             Prod.mk.injEq]
  88
  89/-! ## Independence -/
  90
  91/-- Two recognizers are **independent** if each provides information the other doesn't.
  92    This means: ∃ configs distinguished by r₁ but not r₂, and vice versa. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.