proposition: Lemma in_ultra_setVsetC T (F : set_system T) (A : set T) : UltraFilter F -> F A \/ F (~` A).
proof: Proof. move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right. left; suff : ProperFilter (filter_from (F `|` [set A `&` B | B in F]) id). move=> /max_filter <-; last by move=> B FB; exists B => //; left. by exists A => //; right; exists setT; [apply: filterT|rewrite setIT]. apply: filter_from_proper; last first. move=> B [|[C FC <-]]; first exact: filter_ex. apply: contrapT => /asboolP; rewrite asbool_neg => /forallp_asboolPn AC0. by apply: nFnA; apply: filterS FC => p Cp Ap; apply: (AC0 p). apply: filter_from_filter. by exists A; right; exists setT; [apply: filterT|rewrite setIT]. move=> B C [FB|[DB FDB <-]]. move=> [FC|[DC FDC <-]]; first by exists (B `&` C)=> //; left; apply: filterI. exists (A `&` (B `&` DC)); last by rewrite setICA. by right; exists (B `&` DC) => //; apply: filterI. move=> [FC|[DC FDC <-]]. exists (A `&` (DB `&` C)); last by rewrite setIA. by right; exists (DB `&` C) => //; apply: filterI. exists (A `&` (DB `&` DC)); last by move=> ??; rewrite setIACA setIid. by right; exists (DB `&` DC) => //; apply: filterI. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed