proposition: Lemma EFin_setC T (A : set T) : EFin @` (~` A) = (~` (EFin @` A)) `\` [set -oo; +oo].
proof: Proof. rewrite eqEsubset; split => [_ [r Ar <-]|[r | |]]. by split => [|[]//]; apply: contra_not Ar => -[? ? [] <-]. - move=> [Ar _]; apply/not_exists2P; apply: contra_not Ar => h. by exists r => //; have [|//] := h r; apply: contrapT. - by move=> -[_] /not_orP[_ /=]. - by move=> -[_] /not_orP[/=]. 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