proposition: Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT)) (D : set aT) (f : aT -> rT) : sigma_algebra setT G -> sigma_algebra D (preimage_class D f G).
proof: Proof. case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0. - move=> A; rewrite /preimage_class /= => -[B mB <-{A}]. exists (~` B); first by rewrite -setTD; exact: hC. rewrite predeqE => x; split=> [[Dx Bfx]|[Dx]]; first by split => // -[] _ /Bfx. by move=> /not_andP[]. - move=> F; rewrite /preimage_class /= => mF. have {}mF n : exists x, G x /\ D `&` f @^-1` x = F n. by have := mF n => -[B mB <-]; exists B. have [F' mF'] := @choice _ _ (fun x y => G y /\ D `&` f @^-1` y = F x) mF. exists (\bigcup_k (F' k)); first by apply: hU => n; exact: (mF' n).1. rewrite preimage_bigcup setI_bigcupr; apply: eq_bigcupr => i _. exact: (mF' i).2. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)