search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Do some preparation for the result on sharp elements #274

Closed ayberkt closed 2 months ago

ayberkt commented 2 months ago

This PR is the beginning of the development of the Lawson locale of a Scott domain (#219).

It introduces a new module called LawsonLocale.CompactElementsOfPoint where

  1. the family { c : 𝒦(D) ∣ ↑(c) ∈ F } (on some point F of the Scott locale of a Scott domain D) is defined, and
  2. is proved to be directed.

I will use this when proving that the sharp elements and the spectral points coincide, which should be the next PR on this question.

tomdjong commented 2 months ago

@martinescardo Ayberk isn't done addressing the comments yet (some are still marked as unresolved).

martinescardo commented 2 months ago

"if" should have been "when".

ayberkt commented 2 months ago

I'll get back to this and finish it today.

ayberkt commented 2 months ago

All points have now been addressed and the PR should be ready to merge now.