Zulip Chat Archive

Stream: Is there code for X?

Topic: Closure of set of sets under finite intersections


Adam Topaz (Oct 06 2020 at 21:10):

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 (Oct 06 2020 at 21:13):

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

Reid Barton (Oct 06 2020 at 21:13):

no

Adam Topaz (Oct 06 2020 at 21:15):

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


Last updated: Dec 20 2023 at 11:08 UTC