proposition: Lemma wop_bigU (I : Type) (g : I -> set W) : (forall i, wopen (g i)) -> wopen (\bigcup_i g i).
proof: Proof. move=> gop. set opi := fun i => [set Ui | open Ui /\ g i = f @^-1` Ui]. exists (\bigcup_i get (opi i)). apply: bigcup_open => i. by have /getPex [] : exists U, opi i U by have [U] := gop i; exists U. have g_preim i : g i = f @^-1` (get (opi i)). by have /getPex [] : exists U, opi i U by have [U] := gop i; exists U. rewrite predeqE => s; split=> [[i _]|[i _]]; last by rewrite g_preim; exists i. by rewrite -[_ _]/((f @^-1` _) _) -g_preim; exists i. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed