fact: Definition well_contained (X : CPsMetricSpace) (P Q : X -> CProp) (a : SubPsMetricSpace P) := open Q -> forall H : MStotally_bounded (SubPsMetricSpace P), {r : IR | [0][<]r | forall q : X, infima P (located_imp_located' X P (MStotally_bounded_imp_located X P H)) a q[<=]r -> Q q}.
imports: CoRN.metrics.Prod_Sub