proposition: Lemma maps_compacts_into_strict_imp_weak : forall F, maps_compacts_into F -> maps_compacts_into_weak F.
proof: Proof. intros X HX a b Hab Hinc. destruct (HX a b Hab Hinc) as [c [d [Hcd Hcd0]]]. exists c. exists d. exists (less_leEq _ _ _ Hcd). assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries