structure
definition
def or abbrev
LocalConfigSpace
show as:
view Lean formalization →
formal statement (Lean)
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 :=
proof body
Definition body.
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 :=
66 L.mem_of_mem_N c U hU
67
68/-- If U and V are neighborhoods of c, there's a common refinement -/
69theorem LocalConfigSpace.common_refinement (c : C) (U V : Set C)
70 (hU : U ∈ L.N c) (hV : V ∈ L.N c) :
71 ∃ W ∈ L.N c, W ⊆ U ∧ W ⊆ V := by
72 obtain ⟨W, hW, hWUV⟩ := L.intersection_closed c U V hU hV
73 exact ⟨W, hW, subset_inter_iff.mp hWUV⟩
74
75/-- Points in a neighborhood have sub-neighborhoods -/
76theorem LocalConfigSpace.sub_neighborhood (c c' : C) (U : Set C)
77 (hU : U ∈ L.N c) (hc' : c' ∈ U) :
78 ∃ V ∈ L.N c', V ⊆ U :=
79 L.refinement c U c' hU hc'
80
81/-! ## Neighborhood Filter -/
82
83/-- The neighborhoods of a point form a filter base -/
84def LocalConfigSpace.neighborhoodFilterBase (c : C) : FilterBasis C where
85 sets := L.N c
86 nonempty := L.N_nonempty c
87 inter_sets := by
88 intro U V hU hV
89 obtain ⟨W, hW, hWsub⟩ := L.intersection_closed c U V hU hV
90 exact ⟨W, hW, hWsub⟩
91
92/-- The neighborhood filter at a point -/
93noncomputable def LocalConfigSpace.neighborhoodFilter (c : C) : Filter C :=
94 (L.neighborhoodFilterBase c).filter
95
96/-! ## Discrete Configuration Space -/
97
98/-- A discrete configuration space where every subset is a neighborhood.
99 This is the "maximally fine" locality structure. -/