Intersection can be written as decreasing intersection

Stream: Is there code for X?

[Uni Marx]

Is there something along the lines of ⋂ (x : ↑(Set.Iio S)), f x = ⋂ (x : ↑(Set.Iio S)) (y : ↑(Set.Iio x)), f ↑y in the library?

[Jireh Loreaux]

Probably that fails if the underlying type is something like ℤ.

[Jireh Loreaux]

Or any order where Set.Iio x is not a docs#NoMaxOrder

[Yaël Dillies]

Do you want something like docs#partialSups ?

[Jireh Loreaux]

(As an explicit example of where it fails, consider S := (0 : ℤ), f : ℤ → Set ℤ which sends -1 to ∅ and everything else to Set.univ. Then the left-hand side is empty, but the right-hand side is everything.)

[Uni Marx]

fair - I'm working with conditionally complete lattices with bottom elements either way, but if it takes hypotheses that specific, it's no surprise it's not a thing already

[Antoine Chambert-Loir]

If it's not a thing already, it may be because this is not a thing to use for proofs which work in a large generality, even if this is a thing we pretend using in blackboard proofs (maybe because it makes union/intersection more intuitive).
On the other hand, mathlib provides a lot of API to relate sup, inf`, etc., this is a purely algebraic game to play, and sometimes it is even fun…