proposition: Lemma near_can_continuousAcan_sym f g (x : R) : {near x, cancel f g} -> {near x, continuous f} -> {near f x, continuous g} /\ {near f x, cancel g f}.
proof: Proof. move=> fK fct; near (0 : R)^'+ => e; have e_gt0 : 0 < e by []. have xBeLxDe : x - e <= x + e by rewrite lerD2l gt0_cp. have fcte : {in `[x - e, x + e], continuous f}. by near: e; apply/at_right_in_segment. have fwcte : {within `[x - e, x + e], continuous f}. apply: continuous_in_subspaceT => y yI. by apply: fcte; move/set_mem: yI. have fKe : {in `[x - e, x + e], cancel f g} by near: e; apply/at_right_in_segment. have nearfx : \forall y \near f x, y \in f @`](x - e), (x + e)[. apply: near_in_itv; apply: mono_mem_image_itvoo; last first. by rewrite in_itv/= -ltr_distlC subrr normr0. apply: itv_continuous_inj_mono => //. by apply: (@can_in_inj _ _ _ _ g); near: e; apply/at_right_in_segment. have fxI : f x \in f @`]x - e, x + e[ by exact: (nbhs_singleton nearfx). split; near=> y; first last. rewrite (@segment_continuous_can_sym (x - e) (x + e))//. by apply: subset_itv_oo_cc; near: y. near: y; apply: (filter_app _ _ nearfx); near_simpl; near=> y => yfe. have : {within f @`]x - e, (x + e)[, continuous g}. apply: continuous_subspaceW; last exact: (segment_can_continuous _ fwcte _). exact: subset_itv_oo_cc. rewrite continuous_open_subspace; first by apply; exact: mem_set. exact: interval_open. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)