Zulip Chat Archive

Stream: Is there code for X?

Topic: Closure of set of sets under finite intersections


view this post on Zulip 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)

view this post on Zulip Adam Topaz (Oct 06 2020 at 21:13):

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

view this post on Zulip Reid Barton (Oct 06 2020 at 21:13):

no

view this post on Zulip Adam Topaz (Oct 06 2020 at 21:15):

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


Last updated: May 07 2021 at 20:11 UTC