Stream: General

Topic: Stating that a structure conforms a locale

view this post on Zulip Gergely Buday (Feb 15 2024 at 11:30):

If I have a locale for an algebraic group:

locale group = ...

then what is a good expression of having a geometric structure and proving that it conforms the group laws?

Should I state this that my geometric structure is a sublocale?

sublocale geometric_structure  ⊆ group

? Or something else?

And, what Isar syntax should I use for defining the geometric structure?

Last updated: Feb 28 2025 at 08:24 UTC