proposition: Lemma weak_ent_split A : weak_ent A -> exists2 B, weak_ent B & B \; B `<=` A.
proof: Proof. move=> [B entB sBA]; have : exists C, entourage C /\ C \; C `<=` B. exact/exists2P/entourage_split_ex. case=> C [entC CsubB]; exists ((map_pair f)@^-1` C); first by exists C. by case=> x y [a ? ?]; apply/sBA/CsubB; exists (f a). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed