theorem
proved
composite_comm_indistinguishable
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Composition on GitHub at line 167.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
164 simp [composite_R_eq]
165
166/-- Indistinguishability is symmetric under swap -/
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
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. -/
192theorem composite_info_monotone_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
193 {c₁ c₂ : C} (h : Distinguishable r₁ c₁ c₂) :
194 Distinguishable (r₁ ⊗ r₂) c₁ c₂ :=
195 composite_distinguishes r₁ r₂ (Or.inl h)
196
197theorem composite_info_monotone_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)