def
definition
trivialLocalConfigSpace
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Locality on GitHub at line 112.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
109
110/-- A trivial configuration space where only the whole space is a neighborhood.
111 This is the "maximally coarse" locality structure. -/
112def trivialLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where
113 nonempty := inferInstance
114 N := fun _ => {Set.univ}
115 mem_of_mem_N := fun c U hU => by
116 simp only [Set.mem_singleton_iff] at hU
117 rw [hU]
118 exact mem_univ c
119 N_nonempty := fun _ => ⟨Set.univ, rfl⟩
120 intersection_closed := fun _ U V hU hV => by
121 simp only [Set.mem_singleton_iff] at hU hV
122 subst hU hV
123 exact ⟨Set.univ, rfl, Set.inter_self _ ▸ Subset.rfl⟩
124 refinement := fun _ U _ hU _ => by
125 simp only [Set.mem_singleton_iff] at hU
126 exact ⟨Set.univ, rfl, hU ▸ Subset.rfl⟩
127
128/-! ## Module Status -/
129
130def locality_status : String :=
131 "✓ LocalConfigSpace defined (RG1)\n" ++
132 "✓ Neighborhood axioms: mem_of_mem_N, intersection_closed, refinement\n" ++
133 "✓ Basic lemmas: has_neighborhood, self_mem_neighborhood, common_refinement\n" ++
134 "✓ Neighborhood filter construction\n" ++
135 "✓ Discrete and trivial examples\n" ++
136 "\n" ++
137 "LOCALITY STRUCTURE (RG1) COMPLETE"
138
139#eval locality_status
140
141end RecogGeom
142end IndisputableMonolith