proposition: Lemma preimage_indic (D : set T) (B : set R) : \1_D @^-1` B = if 1 \in B then (if 0 \in B then setT else D) else (if 0 \in B then ~` D else set0).
proof: Proof. rewrite /preimage/= /indic; apply/seteqP; split => x; case: ifPn => B1; case: ifPn => B0 //=. - have [|] := boolP (x \in D); first by rewrite inE. by rewrite notin_set in B0. - have [|] := boolP (x \in D); last by rewrite notin_set. by rewrite notin_set in B1. - by have [xD|xD] := boolP (x \in D); [rewrite notin_set in B1|rewrite notin_set in B0]. - by have [xD|xD] := boolP (x \in D); [rewrite inE in B1|rewrite inE in B0]. - have [xD|] := boolP (x \in D); last by rewrite notin_set. by rewrite inE in B1. - have [|xD] := boolP (x \in D); first by rewrite inE. by rewrite inE in B0. 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