Inductive sets (finiteInterClosure)

Stream: mathlib4

[Yury G. Kudryashov]

Another offender is docs#FiniteInter.finiteInterClosure. It's an inductive predicate of type Set _. @Adam Topaz what do you prefer

• add an auxiliary inductive predicate, then use setOf
• redefine it as a set of intersections of finite subfamilies
• redefine it as the intersection of all sets that contain our set and satisfy the univ and inter properties?

[Adam Topaz]

Yury G. Kudryashov said:

Another offender is docs#FiniteInter.finiteInterClosure. It's an inductive predicate of type Set _. Adam Topaz what do you prefer

• add an auxiliary inductive predicate, then use setOf
• redefine it as a set of intersections of finite subfamilies
• redefine it as the intersection of all sets that contain our set and satisfy the univ and inter properties?

@Yury G. Kudryashov I would prefer making an auxiliary inductive predicate in this case. Do I understand correctly that we are effectively banning the (direct) creation of inductive sets in the sense of inductive foo : Set X where ...?