proposition: Lemma helly3_lifting (T : finType) (P : {set T} -> Prop) : (forall A B, P A -> P B -> P (A :&: B)) -> (forall f : 'I_3 -> {set T}, (forall i, P (f i)) -> (forall i j, f i :&: f j != set0) -> exists x, forall i, x \in f i) -> forall F : {set {set T}}, 0 < #|F| -> (forall A, A \in F -> P A) -> {in F &, forall A B, A :&: B != set0} -> exists x, forall A, A \in F -> x \in A.
proof: Proof. move => closed_P helly3_P. elim/card_ind => /= F IH inh_F F_sub_P F_pw_in. case: (ltnP 1 #|F|) => card_F. - case/card_gt1P : card_F => /= X [Y] [XF YF XY]. move def_F' : ((F :\: [set X;Y]) :|: [set X :&: Y]) => F'. have F'_in_U : (forall A, A \in F' -> P A). { rewrite -def_F'. move => A /setUP [/setDP []|/set1P->]; by auto. } have F'_pw_in : {in F' &, forall A B : {set T}, A :&: B != set0}. { move => A B. rewrite -def_F' !in_setU !in_set1 => HA HB. wlog [HA HB]: A B {HA HB} / A = X :&: Y /\ B \in F. { move => W. case/orP : HA => [/setDP [HA _]|/eqP HA]; case/orP : HB => [/setDP [HB _]|/eqP HB]. - exact: F_pw_in. - rewrite setIC. by apply: W. - exact: W. - rewrite HA HB setIid. exact: F_pw_in. } rewrite HA. pose f := tnth [tuple X; Y; B]. case: (helly3_P f _ _). - apply: ord3P; by rewrite /f /tnth /=; apply: F_sub_P. - do 2 apply: ord3P; by rewrite /f /tnth /=; apply: F_pw_in. - move => x Hx. apply/set0Pn; exists x. rewrite !inE. move: (Hx ord0) (Hx ord1) (Hx ord2). by rewrite /f /tnth /= => -> -> ->. } have card_F' : #|F'| < #|F|. { rewrite -def_F' cardsU cards1. apply: ltn_subn. rewrite -setDDl [#|F|](cardsD1 X) [#|F :\ X|](cardsD1 Y). rewrite !inE XF YF eq_sym XY /= add1n addnC. exact: leqnn. } have inh_F' : 0 < #|F'|. { apply/card_gt0P. exists (X :&: Y). by rewrite -def_F' !inE eqxx. } case: (IH F' _ _ _ _) => // x Hx. exists x => A A_in_F. case: (boolP ((A == X) || (A == Y))) => H. + case : (setIP (Hx (X :&: Y) _)). * by rewrite -def_F' !inE eqxx. * by case/orP: H => /eqP ->. + apply: Hx. by rewrite -def_F' !inE H A_in_F. - have/card1P [A HA] : #|F| == 1 by rewrite eqn_leq card_F. move: (F_pw_in A A). rewrite !HA inE eqxx. case/(_ _ _)/Wrap => //. case/set0Pn => x. rewrite setIid => Hx. exists x => B. by rewrite HA inE => /eqP->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph set_tac)