theorem
proved
composite_comm_events
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 162.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
159/-! ## Associativity and Commutativity -/
160
161/-- Composition is commutative up to isomorphism on events -/
162theorem composite_comm_events (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
163 (r₁ ⊗ r₂).R c = Prod.swap ((r₂ ⊗ r₁).R c) := by
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₂)