proposition: Theorem inf_induced2 r A F: order r -> sub F (substrate r) -> sub A F -> has_infimum r A -> inc (infimum r A) F -> (has_infimum (induced_order r F) A /\ infimum r A = infimum (induced_order r F) A).
proof: Proof. move=> or Fs AF hsA sAF. have [oi si]:= (iorder_osr or Fs). have As: sub A (substrate r) by apply: sub_trans Fs. have Asi:sub A (substrate (induced_order r F)) by ue. have lub:=(infimum_pr1 or hsA). have lubi: greatest_lower_bound (induced_order r F) A (infimum r A). move: lub => /(glbP or As) [[us ub] lub]; apply/(glbP oi Asi). split. split; [by rewrite si| move=> y yA; apply/iorder_gle0P; fprops]. move=> z []; rewrite si // => zF zub. apply/iorder_gle0P; fprops; apply: lub; split; first by apply: Fs. move=> y yA; move: (zub _ yA); apply:iorder_gle1. have aux: has_infimum (induced_order r F) A by exists (infimum r A). split=>//;apply: (infimum_unique oi lubi (infimum_pr1 oi aux)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)