Theory Transport_Compositions_Agree_Monotone

✐‹creator "Kevin Kappelmann"›
subsection ‹Monotonicity›
theory Transport_Compositions_Agree_Monotone
  imports
    Transport_Compositions_Agree_Base
begin

context transport_comp_agree
begin

lemma mono_wrt_rel_leftI:
  assumes "((≤L1)  (≤R1)) l1" "((≤L2)  (≤R2)) l2"
  and "x y. xL1 y  l1 xR1 l1 y  l1 xL2 l1 y"
  shows "((≤L)  (≤R)) l"
  unfolding left_eq_comp using assms by (urule dep_mono_wrt_rel_compI)

end

context transport_comp_same
begin

lemma mono_wrt_rel_leftI:
  assumes "((≤L1)  (≤R1)) l1" "((≤R1)  (≤R2)) l2"
  shows "((≤L)  (≤R)) l"
  using assms by (rule mono_wrt_rel_leftI) auto

end


end