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