proposition: Lemma LposPartStable : forall {Elem : FunctionRieszSpace} (f : PartialFunction (X Elem)) (fL : L Elem f), L Elem (XposPart f).
proof: Proof. intros. unfold XposPart. apply LscaleStable. apply LplusStable. assumption. apply LabsStable. assumption. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions