proposition: Lemma ysection_indic (R : ringType) T1 T2 (A : set (T1 * T2)) y : ysection A y = (fun x => (\1_A (x, y) : R)) @^-1` [set 1].
proof: Proof. apply/seteqP; split => [x/mem_set/=|x/=]; rewrite indicE. by rewrite mem_ysection => ->. by rewrite /ysection/=; case: (_ \in _) => //= /esym/eqP /[!oner_eq0]. 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