Theory Rank_Nullity_Theorem.Dual_Order
section "Dual Order"
theory Dual_Order
imports Main
begin
subsection‹Interpretation of dual wellorder based on wellorder›
lemma wf_wellorderI2:
assumes wf: "wf {(x::'a::ord, y). y < x}"
assumes lin: "class.linorder (λ(x::'a) y::'a. y ≤ x) (λ(x::'a) y::'a. y < x)"
shows "class.wellorder (λ(x::'a) y::'a. y ≤ x) (λ(x::'a) y::'a. y < x)"
using lin unfolding class.wellorder_def apply (rule conjI)
apply (rule class.wellorder_axioms.intro) by (blast intro: wf_induct_rule [OF wf])