def
definition
def or abbrev
trivialLocalConfigSpace
show as:
view Lean formalization →
formal statement (Lean)
112def trivialLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where
113 nonempty := inferInstance
proof body
Definition body.
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