proposition: Lemma smallest_filter_finI {T : choiceType} (D : set T) f : filter_from (finI_from D f) id = smallest (@Filter T) (f @` D).
proof: Proof. by rewrite filterI_iter_finI filterI_iterE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed