theorem
proved
tactic proof
composite_comm_indistinguishable
show as:
view Lean formalization →
formal statement (Lean)
167theorem composite_comm_indistinguishable (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
168 (c₁ c₂ : C) :
169 Indistinguishable (r₁ ⊗ r₂) c₁ c₂ ↔ Indistinguishable (r₂ ⊗ r₁) c₁ c₂ := by
proof body
Tactic-mode proof.
170 rw [composite_indistinguishable_iff, composite_indistinguishable_iff]
171 exact And.comm
172
173/-! ## N-ary Composition -/
174
175/-- Triple composite recognizer -/
176def CompositeRecognizer₃ {E₃ : Type*}
177 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (r₃ : Recognizer C E₃) :
178 Recognizer C (E₁ × E₂ × E₃) where
179 R := fun c => (r₁.R c, r₂.R c, r₃.R c)
180 nontrivial := by
181 obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
182 use c₁, c₂
183 intro heq
184 apply hne
185 simp only [Prod.mk.injEq] at heq
186 exact heq.1
187
188/-! ## Information Content -/
189
190/-- The composite recognizer has at least as much information as either component.
191 "Information" here means the ability to distinguish configurations. -/