proposition: Lemma Exercise1_22D r F: order r -> cofinal r F -> order_isomorphism (Lf (fun z => z \cap F) (reg_opens r) (reg_opens (induced_order r F))) (reg_open_order r)(reg_open_order (induced_order r F)).
proof: Proof. move=> or cF. have Fs: (sub F (substrate r)) by move: cF => [ok _]. move: (iorder_osr or Fs) => []. set (r':= induced_order r F)=> oir sr'. have oi: (forall x, open_r r x -> open_r r' (x \cap F)). move=> x ox; apply: (Exercise1_22B or cF ox). have ta: (lf_axiom (fun z => z \cap F) (reg_opens r) (reg_opens r')). move=> t => /Zo_P [] /setP_P tsr ot; apply: Zo_i; fprops; apply /setP_P. rewrite sr'; apply: subsetI2r. set (g:=Lf (fun z : Set => z \cap F) (reg_opens r) (reg_opens r')). have bg: (bijection g). rewrite /g; apply: lf_bijective => //. move=> u v => /Zo_P [] /setP_P usr ou /Zo_P [] /setP_P vsr ov si. apply: extensionality. apply: (Exercise1_22C (U:=u) (U':=v) or cF) => //; rewrite si; fprops. apply: (Exercise1_22C (U:=v) (U':=u) or cF) => //; rewrite - si; fprops. move=> y /Zo_P [] /setP_P ysr' oy. have ysr: (sub y (substrate r)) by apply: (@sub_trans F) => //; ue. set (x1:= Zo (substrate r) (fun z => exists2 x, inc x y& gle r x z)). have x1sr: (sub x1 (substrate r)) by apply: Zo_S. have yx1: (sub y x1). by move=> t ty; move: (ysr _ ty)=> tsr;apply: Zo_i =>//; ex_tac; order_tac. have ox1: (open_o r x1). split => // a b /Zo_P [asr [c cy ca]] ab; apply /Zo_P. split; [ order_tac | ex_tac; order_tac]. set (x2:= open_bar r x1). have x2F: (sub y (x2 \cap F)). move=> t ty; apply: setI2_i. by apply: (Exercise1_22e or ox1); apply: yx1. by rewrite - sr'; apply: ysr'. move:(Exercise1_22i or ox1) => ob; exists (open_bar r x1). by apply: Zo_i => //; apply /setP_P; apply: Exercise1_22f. apply: extensionality => // x /setI2_P [xb xF]. rewrite (Exercise1_22p oir oy); apply:Exercise1_22h => //;[by case: oy | ue|]. move=> z xz; move: (iorder_gle1 xz) => xz1. have : (inc z (open_bar r x1)) by move: ob =>[[_ h] _]; apply: (h _ _ xb xz1). move /setU_P => [t zt] /Zo_P [] /setP_P tsr [ot]. move /(cofinal_inducedP or tsr) => [x1t x1p]. move: (x1p _ zt) => [x3 yx3 xy3]. move: yx3 => /Zo_P [x3s [x4 x4y x4x3]]. move: cF => [_ cF]; move: (cF _ x3s) => [x5 x5F x35]. have r45: (gle r' x4 x5). apply /iorder_gle0P => //; [ by rewrite - sr'; apply: ysr' | order_tac]. exists x5=> //; first by move:oy => [[_ oy] _]; apply: (oy _ _ x4y r45). apply /iorder_gle0P => //; [rewrite - sr'; order_tac | order_tac ]. rewrite /reg_open_order /g. split => //; fprops. rewrite !(proj2 (sub_osr _)); saw. hnf; aw;move => x y xsr ysr; rewrite !LfV//; split. move /sub_gleP => [i1 i2 i3]; apply /sub_gleP;split; fprops. by move=> t /setI2_P [tx tF]; apply/setI2_P;split => //; apply: i3. move /sub_gleP => [i1 i2 i3]; apply /sub_gleP;split => //. move: xsr ysr => /Zo_P [_ i4] /Zo_P [_ i5]. apply: (Exercise1_22C or cF i4 i5 i3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)