proposition: Lemma left_right_continuousP {T : topologicalType} (f : R -> T) x : f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.
proof: Proof. split; last by move=> cts; split; exact: cvg_within_filter. move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real. move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//]. - by move=> <-; exact: nbhs_singleton. - by move=> ->; exact: nbhs_singleton. 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)