proposition: Lemma lower_semicontinuousP f : lower_semicontinuous f <-> forall a, open [set x | f x > a%:E].
proof: Proof. split=> [sci a|openf x a afx]. rewrite openE /= => x /= /sci[A + Aaf]; rewrite nbhsE /= => -[B xB BA]. apply: nbhs_singleton; apply: nbhs_interior. by rewrite nbhsE /=; exists B => // y /BA /=; exact: Aaf. exists [set x | a%:E < f x] => //. by rewrite nbhsE/=; exists [set x | a%:E < f x]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule