proposition: Lemma bigcup_set0 i (D : I -> {set B}) (F : B -> I -> {set A}) b : b \in D i -> F b i != set0 -> \bigcup_(b' in D i) F b' i == set0 -> D i == set0.
proof: Proof. move=> bDi Fbi0 /set0Pn F0; apply/set0Pn => -[b' b'i]; apply F0 => {F0}. by case/set0Pn : Fbi0 => a tA; exists a; apply/bigcupP; exists b. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext