Stream: Beginner Questions

Topic: sublocale

zibo yang (Apr 21 2021 at 14:38):

how can I specifiy is_open:: 'a => bool when I want to prove something like:sublocal real_vector_normed_space $\subseteq$ topological_space

Manuel Eberl (Apr 21 2021 at 14:49):

I'm afraid I don't understand your question at all.

Anthony Bordg (Apr 21 2021 at 14:49):

Use the $\lambda$ notation.

Manuel Eberl (Apr 21 2021 at 14:52):

Ah, I only realised now that you're talking about that new AFP entry on schemes…

Manuel Eberl (Apr 21 2021 at 14:52):

I thought you were talking about the corresponding notions from the standard library.

zibo yang (Apr 21 2021 at 14:54):

but I fail to make it when I code like
'''sublocale real_normed_vector_space ⊆ topological_space
where "is_open ≡ λ a::'a set.0"
'''

Anthony Bordg (Apr 21 2021 at 14:55):

@zibo yang 0 is not a boolean.

zibo yang (Apr 21 2021 at 14:56):

sorry but it fails again when I change it to true

zibo yang (Apr 21 2021 at 14:59):

actually I succeed proving:
sublocale real_normed_vector_space ⊆ sub: topological_space "is_open_space"
after I specify is_open_space in the context of real_normed_vector_space

zibo yang (Apr 21 2021 at 15:00):

but I always fail to define is_open when facing
sublocale real_normed_vector_space ⊆ topological_space

zibo yang (Apr 21 2021 at 15:19):

what causes my confusion is that: I code:

proof(unfold_locales)```
then I get the proof state:

proof (state)
goal (3 subgoals):

1. open UNIV

2. ⋀S T. open S ⟹
   open T ⟹
   open
   (S ∩ T)

3. ⋀K. ∀S∈K.
   open S ⟹
   open (⋃ K)

I am confused about:1. I don't see any function named "open", there is only "is_open"
2. I get failure when I print "using open_def" to get the definition of "open"
3. I cannot define it like

where "open = is_open_space"

zibo yang (Apr 21 2021 at 15:22):

what causes my confusion is that: I code:

sublocale real_normed_vector_space ⊆ topological_space
proof(unfold_locales)

then I get the proof state:

proof (state)
goal (3 subgoals):
 1. open UNIV
 2. ⋀S T. open S ⟹
           open T ⟹
           open
(S ∩ T)
 3. ⋀K. ∀S∈K.
open S ⟹
         open (⋃ K)

I am confused about:1. I don't see any function named "open", there is only "is_open"

2. I get failure when I print "using open_def" to get the definition of "open"
3. I cannot define it like

where "open = is_open_space"

zibo yang (Apr 21 2021 at 15:27):

so I guess the only way to define "is_open" is just to specify it after the name"topological_space" like:

sublocale real_normed_vector_space ⊆ sub: topological_space "is_open_space"

zibo yang (Apr 21 2021 at 15:28):

am I right?

Anthony Bordg (Apr 21 2021 at 16:05):

@zibo yang It seems like your topological spaces are the ones from the standard library, not the ones from the development on schemes. So, you may have to use a prefix to disambiguate. If your problem persists, I propose to continue the discussion elsewhere, since it's not a question on sublocales per se.

Last updated: Dec 21 2024 at 16:20 UTC