fact: Definition closed_fam_of (A : set T) I (D : set I) (f : I -> set T) := exists2 g : I -> set T, (forall i, D i -> closed (g i)) & forall i, D i -> f i = A `&` g i.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed