proposition: Lemma inverse_image_union: forall {X Y:Type} (f:X->Y) (T1 T2:Ensemble Y), inverse_image f (Union T1 T2) = Union (inverse_image f T1) (inverse_image f T2).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. destruct H. inversion H. left; constructor; trivial. right; constructor; trivial. constructor. destruct H as [? []|? []]. left; trivial. right; trivial. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec