proposition: Theorem inf_induced1 r A F: order r -> sub F (substrate r) -> sub A F -> has_infimum r A -> has_infimum (induced_order r F) A -> gle r (infimum (induced_order r F) A) (infimum r A).
proof: Proof. move=> or Fs AF sA siA. 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. move: (infimum_pr1 or sA) (infimum_pr1 oi siA). set (u:= infimum r A). set (v:=infimum (induced_order r F) A). move=> /(glbP or As) [ub lub] /(glbP oi Asi) [[us ubi] lubi]; apply: lub. move: us; rewrite si => vF. split;[ by apply: Fs | move=> y yA; move: (ubi _ yA); apply:iorder_gle1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)