Closure of set of sets under finite intersections

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have a construction like this?

inductive fin_inter {α : Type*} (S : set (set α)) : set (set α)
| of {T} : T ∈ S → fin_inter T
| inter {T1 T2} : fin_inter T1 → fin_inter T2 → fin_inter (T1 ∩ T2)

[Adam Topaz]

docs#filter.generate_sets is close, but has too much.

[Reid Barton]

no

[Adam Topaz]

(yeah I guess I forgot the empty intersection is set.univ :))