proposition: Lemma inverse_image_add {X Y : Type} (f : X -> Y) (g : Y -> X) (F : Family Y) (T : Ensemble Y) : (forall x, g (f x) = x) -> (forall y, f (g y) = y) -> inverse_image (inverse_image g) (Add F T) = Add (inverse_image (inverse_image g) F) (inverse_image f T).
proof: Proof. intros Hgf Hfg. apply Extensionality_Ensembles. rewrite inverse_image_fun, inverse_image_fun. split; red; intros; inversion H; subst; (left; assumption) + (right; inversion H0; rewrite inverse_image_id; constructor + assumption). Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies