fact: Definition near_covering_within (K : set X) := forall (I : Type) (F : set_system I) (P : I -> X -> Prop), Filter F -> (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') -> \near F, K `<=` P F.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed