frames

Stream: general

[Johan Commelin]

Are frames in mathlib? https://ncatlab.org/nlab/show/frame

[Johan Commelin]

I quote:

A frame O is a poset that has
all small coproducts, called joins ⋁
all finite limits, called meets ∧
and which satisfies the infinite distributive law:
x∧(⋁iyi)≤⋁i(x∧yi)
for all x,{yi}i in A
(Note that the converse holds in any case, so we have equality.)

[Johan Commelin]

Seems like we have all the ingredients.

[Johan Commelin]

Note that the notion dual to a frame is called a locale and these are the gadgets that people use to do topology without points. It seems that mathlib is also fond of doing topology without points, so maybe there is a general interest for these things.