proposition: Lemma EFin_bigcup T (F : nat -> set T) : EFin @` (\bigcup_i F i) = \bigcup_i (EFin @` F i).
proof: Proof. rewrite eqEsubset; split => [_ [r [n _ Fnr <-]]|]; first by exists n => //; exists r. by move=> x [n _ [r Fnr <- /=]]; exists r => //; exists n. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal