proposition: Lemma filterI_iterE {T : Type} (F : set (set T)) : smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id.
proof: Proof. rewrite eqEsubset; split. apply: smallest_sub => //; first last. by move=> A FA; exists A => //; exists O => //; right. apply: filter_from_filter; first by exists setT; exists O => //; left. move=> P Q [i _ sFP] [j _ sFQ]; exists (P `&` Q) => //. exists (maxn i j).+1 => //=; exists P. by apply: filterI_iter_sub; first exact: leq_maxl. by exists Q => //; apply: filterI_iter_sub; first exact: leq_maxr. move=> + [+ [n _]]; elim: n => [A B|n IH/= A B]. move=> [-> /[!(@subTset T)] ->|]; first exact: filterT. by move=> FB /filterS; apply; apply: sub_gen_smallest. move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB. by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed