proposition: Lemma inf_funP r f: order r -> substrate r = target f -> function f -> forall x, (inf_funp r f x <-> [/\ inc x (target f), (forall a, inc a (source f) -> gle r x (Vf f a)) & forall z, inc z (target f) -> (forall a, inc a (source f) -> gle r z (Vf f a)) -> gle r z x]).
proof: Proof. move=> or sr ff x. have si: sub (Imf f) (substrate r). by rewrite sr; apply: fun_image_Starget1. have gf: sgraph (graph f) by fprops. apply: (iff_trans (glbP or si x)); split. move=> [[xt p1] p2]; split => //; first by ue. move=> a afs; apply: p1; first by apply/(Imf_P ff);ex_tac. move=> z zt sh; apply: p2; split; first by ue. by move=> y /(Imf_P ff) [u usf ->]; apply: sh. move=> [xt p1 p2];split. split; first by ue. by move=> yy/(Imf_P ff) [u usf ->]; apply: p1. move=> z [ztg p3]; apply: p2; first by ue. move=> a asf; apply: p3; apply /(Imf_P ff); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)