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)
40def CompositeRecognizer (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
41 Recognizer C (E₁ × E₂) where
42 R := fun c => (r₁.R c, r₂.R c)
proof body
Definition body.
43 nontrivial := by
44 -- Use nontriviality of r₁ to construct distinct events
45 obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
46 use c₁, c₂
47 intro heq
48 apply hne
49 exact (Prod.mk.injEq _ _ _ _).mp heq |>.1
50
51/-- Notation for composite recognizer -/
52infixl:70 " ⊗ " => CompositeRecognizer
53
54/-! ## Refinement Properties -/
55
56/-- The composite recognizer's map is the product of component maps -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
nontrivial
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
mk
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
mk
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
map
in IndisputableMonolith.Measurement.RSNative.Core
decl_use