Theory Binary_Relations_Order_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Order›
theory Binary_Relations_Order_Base
  imports
    Binary_Relation_Functions
    HOL.Orderings
begin

lemma le_relI [intro]:
  assumes "⋀x y. R x y ⟹ S x y"
  shows "R ≤ S"
  using assms by (rule predicate2I)

lemma le_relD [dest]:
  assumes "R ≤ S"
  and "R x y"
  shows "S x y"
  using assms by (rule predicate2D)

lemma le_relE:
  assumes "R ≤ S"
  obtains "⋀x y.  R x y ⟹ S x y"
  using assms by blast

end