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⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘L2⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  and "⋀x y. x ≤⇘L1⇙ y ⟹ l1 x ≤⇘R1⇙ l1 y ⟹ l1 x ≤⇘L2⇙ l1 y"
  shows "((≤⇘L⇙) ⇛⇩m (≤⇘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⇙) ⇛⇩m (≤⇘R1⇙)) l1" "((≤⇘R1⇙) ⇛⇩m (≤⇘R2⇙)) l2"
  shows "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  using assms by (rule mono_wrt_rel_leftI) auto

end


end