proposition: Lemma open_fromI (A B : set T) : open_from A -> open_from B -> open_from (A `&` B).
proof: Proof. move=> [DA sDAD AeUbA] [DB sDBD BeUbB]. have ABU : forall t, (A `&` B) t -> exists it, D it /\ b it t /\ b it `<=` A `&` B. move=> t [At Bt]. have [iA [DiA [biAt sbiA]]] : exists i, D i /\ b i t /\ b i `<=` A. move: At; rewrite -AeUbA => - [i DAi bit]; exists i. by split; [apply: sDAD|split=> // ?; exists i]. have [iB [DiB [biBt sbiB]]] : exists i, D i /\ b i t /\ b i `<=` B. move: Bt; rewrite -BeUbB => - [i DBi bit]; exists i. by split; [apply: sDBD|split=> // ?; exists i]. have [i [Di bit sbiAB]] := b_join DiA DiB biAt biBt. by exists i; split=> //; split=> // s /sbiAB [/sbiA ? /sbiB]. set Dt := fun t => [set it | D it /\ b it t /\ b it `<=` A `&` B]. exists [set get (Dt t) | t in A `&` B]. by move=> _ [t ABt <-]; have /ABU/getPex [] := ABt. rewrite predeqE => t; split=> [[_ [s ABs <-] bDtst]|ABt]. by have /ABU/getPex [_ [_]] := ABs; apply. by exists (get (Dt t)); [exists t| have /ABU/getPex [? []]:= ABt]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed