proposition: Lemma LminStable : forall {Elem : FunctionRieszSpace} (f g : PartialFunction (X Elem)) (fL : L Elem f) (gL : L Elem g), L Elem (Xmin f g).
proof: Proof. intros. apply LminusStable. assumption. apply LnegPartStable. apply LminusStable. assumption. assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions