proposition: Lemma restrict_indic T (R : numFieldType) (E A : set T) : ((\1_E : T -> R) \_ A) = \1_(E `&` A).
proof: Proof. apply/funext => x; rewrite /restrict 2!indicE. case: ifPn => [|] xA; first by rewrite in_setI xA andbT. by rewrite in_setI (negbTE xA) andbF. 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