proposition: Lemma open_from_bigU (I0 : Type) (f : I0 -> set T) : (forall i, open_from (f i)) -> open_from (\bigcup_i f i).
proof: Proof. set fop := fun j => [set Dj | Dj `<=` D /\ f j = \bigcup_(i in Dj) b i]. exists (\bigcup_j get (fop j)). move=> i [j _ fopji]. suff /getPex [/(_ _ fopji)] : exists Dj, fop j Dj by []. by have [Dj] := H j; exists Dj. rewrite predeqE => t; split=> [[i [j _ fopji bit]]|[j _]]. exists j => //; suff /getPex [_ ->] : exists Dj, fop j Dj by exists i. by have [Dj] := H j; exists Dj. have /getPex [_ ->] : exists Dj, fop j Dj by have [Dj] := H j; exists Dj. by move=> [i]; exists i => //; exists j. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed