structure
definition
def or abbrev
LocalRecognizer
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Definition body.
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 -/
65
66/-- The local image of a recognizer on a neighborhood -/
67def Recognizer.localImage (r : Recognizer C E) (U : Set C) : Set E :=
68 r.R '' U
69
70/-- Local image is subset of full image -/
71theorem Recognizer.localImage_subset_range (r : Recognizer C E) (U : Set C) :
72 r.localImage U ⊆ Set.range r.R :=
73 Set.image_subset_range r.R U
74
75/-! ## Preimage Structure -/
76
77/-- The preimage (fiber) of an event under a recognizer -/
78def Recognizer.fiber (r : Recognizer C E) (e : E) : Set C :=
79 r.R ⁻¹' {e}
80
81/-- A configuration is in the fiber of its event -/
82theorem Recognizer.mem_fiber_self (r : Recognizer C E) (c : C) :
83 c ∈ r.fiber (r.R c) := by
84 simp [fiber]
85
86/-- Fibers partition the configuration space -/
87theorem Recognizer.fibers_partition (r : Recognizer C E) :
88 ∀ c : C, ∃! e : E, c ∈ r.fiber e := by
89 intro c
90 use r.R c
91 constructor
92 · exact r.mem_fiber_self c
93 · intro e he
94 simp [fiber] at he
95 exact he.symm
96
97/-! ## Event Lifting -/
98
99/-- An event is realized by some configuration if it's in the image -/
100def Recognizer.isRealized (r : Recognizer C E) (e : E) : Prop :=
101 e ∈ Set.range r.R
102
103/-- Every event in the image has a witness configuration -/
104noncomputable def Recognizer.witness (r : Recognizer C E) (e : E)
105 (he : r.isRealized e) : C :=
106 he.choose
107
108theorem Recognizer.witness_spec (r : Recognizer C E) (e : E)
109 (he : r.isRealized e) : r.R (r.witness e he) = e :=
110 he.choose_spec
111
112/-! ## Constant Recognizer (Trivial Event Space) -/
113
114/-- A constant function is NOT a valid recognizer (it's trivial) -/