structure
definition
LocalConfigSpace
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 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
32
33 The neighborhoods allow us to talk about "nearby" configurations
34 without assuming a metric or full topology. -/
35structure LocalConfigSpace (C : Type*) extends ConfigSpace C where
36 /-- Neighborhood assignment: for each c, a family of "local" sets around c -/
37 N : C → Set (Set C)
38
39 /-- Every neighborhood of c contains c -/
40 mem_of_mem_N : ∀ c U, U ∈ N c → c ∈ U
41
42 /-- Neighborhoods are nonempty for each point -/
43 N_nonempty : ∀ c, (N c).Nonempty
44
45 /-- Intersection closure: if U, V ∈ N(c) both contain c, then there exists
46 W ∈ N(c) with W ⊆ U ∩ V -/
47 intersection_closed : ∀ c U V, U ∈ N c → V ∈ N c →
48 ∃ W ∈ N c, W ⊆ U ∩ V
49
50 /-- Refinement: if U ∈ N(c) and c' ∈ U, then there exists V ∈ N(c')
51 with V ⊆ U -/
52 refinement : ∀ c U c', U ∈ N c → c' ∈ U →
53 ∃ V ∈ N c', V ⊆ U
54
55/-! ## Basic Lemmas -/
56
57variable {C : Type*} (L : LocalConfigSpace C)
58
59/-- Every configuration has at least one neighborhood -/
60theorem LocalConfigSpace.has_neighborhood (c : C) : (L.N c).Nonempty :=
61 L.N_nonempty c
62
63/-- Every point is in its own neighborhoods -/
64theorem LocalConfigSpace.self_mem_neighborhood (c : C) (U : Set C) (hU : U ∈ L.N c) :
65 c ∈ U :=