proposition: Lemma image_indic D A : \1_D @` A = (if A `\` D != set0 then [set 0] else set0) `|` (if A `&` D != set0 then [set 1 : R] else set0).
proof: Proof. rewrite /indic; apply/predeqP => x; split => [[t At /= <-]|]. by rewrite /indic; case: (boolP (t \in D)); rewrite ?(inE, notin_set) => Dt; [right|left]; rewrite ifT//=; apply/set0P; exists t. by move=> []; case: ifPn; rewrite ?negbK// => /set0P[t [At Dt]] ->; exists t => //; case: (boolP (t \in D)); rewrite ?(inE, notin_set). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences