proposition: Lemma d_restriction_metric_open_ball (p : FT) (r : R) : open_ball d_restriction p r = inverse_image (@proj1_sig X F) (open_ball d (proj1_sig p) r).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct H. constructor. constructor. assumption. - destruct H. destruct H. constructor. assumption. Qed.
imports: Topology(RationalsInReals SubspaceTopology) ZornsLemma(EnsemblesTactics DecidableDec) Coq(Reals ClassicalChoice Program.Subset) Coq(Lia Lra)