structure
definition
Recognizer
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogGeom.Recognizer on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
31 to the observable event world.
32
33 RG2: There exists at least one nontrivial recognizer. -/
34structure Recognizer (C : Type*) (E : Type*) where
35 /-- The recognition function mapping configurations to events -/
36 R : C → E
37 /-- The recognizer is nontrivial: at least two distinct events are produced -/
38 nontrivial : ∃ c₁ c₂ : C, R c₁ ≠ R c₂
39
40/-- A local recognizer is a recognizer on a local configuration space -/
41structure LocalRecognizer (C : Type*) (E : Type*) extends
42 LocalConfigSpace C, Recognizer C E
43
44/-! ## Basic Properties -/
45
46variable {C E : Type*}
47
48/-- The image of a recognizer has at least 2 elements -/
49theorem Recognizer.image_nontrivial (r : Recognizer C E) :
50 ∃ e₁ e₂ : E, e₁ ∈ Set.range r.R ∧ e₂ ∈ Set.range r.R ∧ e₁ ≠ e₂ := by
51 obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
52 exact ⟨r.R c₁, r.R c₂, ⟨c₁, rfl⟩, ⟨c₂, rfl⟩, hne⟩
53
54/-- A trivial recognizer maps everything to the same event -/
55def Recognizer.isTrivial (r : Recognizer C E) : Prop :=
56 ∀ c₁ c₂ : C, r.R c₁ = r.R c₂
57
58/-- No recognizer is trivial (by definition) -/
59theorem Recognizer.not_trivial (r : Recognizer C E) : ¬r.isTrivial := by
60 intro h
61 obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
62 exact hne (h c₁ c₂)
63
64/-! ## Local Image -/