100def discreteLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where 101 nonempty := inferInstance
proof body
Definition body.
102 N := fun c => {U : Set C | c ∈ U} 103 mem_of_mem_N := fun c U hU => hU 104 N_nonempty := fun c => ⟨Set.univ, mem_univ c⟩ 105 intersection_closed := fun c U V hU hV => ⟨U ∩ V, ⟨hU, hV⟩, Subset.rfl⟩ 106 refinement := fun c U c' hU hc' => ⟨U, hc', Subset.rfl⟩ 107 108/-! ## Trivial Configuration Space -/ 109 110/-- A trivial configuration space where only the whole space is a neighborhood. 111 This is the "maximally coarse" locality structure. -/
depends on (16)
Lean names referenced from this declaration's body.