Theory Closure_Operators

(* 
  Title: Closure and Co-Closure Operators
  Author: Georg Struth 
  Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Closure and Co-Closure Operators›

theory Closure_Operators
  imports Galois_Connections 

begin

subsection ‹Closure Operators›

text ‹Closure and coclosure operators in orders and complete lattices are defined in this section,
and some basic properties are proved. Isabelle infers the appropriate types. Facts are 
taken mainly from the Compendium of Continuous Lattices~\<^cite>‹"GierzHKLMS80"› and 
Rosenthal's book on quantales~\<^cite>‹"Rosenthal90"›.›

definition clop :: "('a::order ⇒ 'a) ⇒ bool" where
  "clop f = (id ≤ f ∧ mono f ∧ f ∘ f ≤ f)"

lemma clop_extensive: "clop f ⟹ id ≤ f"
  by (simp add: clop_def)

lemma clop_extensive_var: "clop f ⟹ x ≤ f x"
  by (simp add: clop_def le_fun_def)

lemma clop_iso: "clop f ⟹ mono f"
  by (simp add: clop_def)

lemma clop_iso_var: "clop f ⟹ x ≤ y ⟹ f x ≤ f y"
  by (simp add: clop_def mono_def)

lemma clop_idem: "clop f ⟹ f ∘ f = f"
  by (simp add: antisym clop_def le_fun_def)

lemma clop_Fix_range: "clop f ⟹ (Fix f = range f)"
  by (simp add: clop_idem retraction_prop_fix)

lemma clop_idem_var: "clop f ⟹ f (f x) = f x"
  by (simp add: clop_idem retraction_prop)

lemma clop_Inf_closed_var: 
  fixes f :: "'a::complete_lattice ⇒ 'a" 
  shows "clop f ⟹ f ∘ Inf ∘ (`) f  = Inf ∘ (`) f"    
  unfolding clop_def mono_def comp_def le_fun_def 
  by (metis (mono_tags, lifting) antisym id_apply le_INF_iff order_refl)

lemma clop_top:
  fixes f :: "'a::complete_lattice ⇒ 'a"
  shows "clop f ⟹ f ⊤ = ⊤"
  by (simp add: clop_extensive_var top.extremum_uniqueI)

lemma "clop (f::'a::complete_lattice ⇒ 'a) ⟹ f (⨆x ∈ X. f x) = (⨆x ∈ X. f x)" (*nitpick*)
  oops

lemma "clop (f::'a::complete_lattice ⇒ 'a) ⟹ f (f x ⊔ f y) = f x ⊔ f y" (*nitpick*)
  oops

lemma  "clop (f::'a::complete_lattice ⇒ 'a) ⟹ f ⊥ = ⊥" (*nitpick *)
  oops
  
lemma "clop (f::'a set ⇒ 'a set) ⟹ f (⨆x ∈ X. f x) = (⨆x ∈ X. f x)" (*nitpick*)
  oops

lemma "clop (f::'a set ⇒ 'a set) ⟹ f (f x ⊔ f y) = f x ⊔ f y" (*nitpick*)
  oops

lemma  "clop (f::'a set ⇒ 'a set) ⟹ f ⊥ = ⊥" (*nitpick *)
  oops

lemma clop_closure: "clop f ⟹ (x ∈ range f) = (f x = x)"
  by (simp add: clop_idem retraction_prop)

lemma clop_closure_set: "clop f ⟹ range f = Fix f"
  by (simp add: clop_Fix_range)

lemma clop_closure_prop: "(clop::('a::complete_lattice_with_dual⇒ 'a) ⇒ bool) (Inf ∘ ↑)"
  by (simp add: clop_def mono_def)

lemma clop_closure_prop_var: "clop (λx::'a::complete_lattice. ⨅{y. x ≤ y})"
  unfolding clop_def comp_def le_fun_def mono_def by (simp add: Inf_lower le_Inf_iff)

lemma clop_alt: "(clop f) = (∀x y. x ≤ f y ⟷ f x ≤ f y)"
  unfolding clop_def mono_def le_fun_def comp_def id_def by (meson dual_order.refl order_trans)

text ‹Finally it is shown that adjoints in a Galois connection yield closure operators.›

lemma clop_adj: 
  fixes f :: "'a::order ⇒ 'b::order"
  shows "f ⊣ g ⟹ clop (g ∘ f)"
  by (simp add: adj_cancel2 adj_idem2 adj_iso4 clop_def)

text ‹Closure operators are monads for posets, and monads arise from adjunctions. 
This fact is not formalised at this point. But here is the first step: every function 
can be decomposed into a surjection followed by an injection.›

definition "surj_on f Y = (∀y ∈ Y. ∃x. y = f x)"

lemma surj_surj_on: "surj f ⟹ surj_on f Y"
  by (simp add: surjD surj_on_def)

lemma fun_surj_inj: "∃g h. f = g ∘ h ∧ surj_on h (range f) ∧ inj_on g (range f)"
proof-
  obtain h where a: "∀x. f x = h x"
    by blast
  then have "surj_on h (range f)"
    by (metis (mono_tags, lifting) imageE surj_on_def)
  then show ?thesis
    unfolding inj_on_def surj_on_def fun_eq_iff using a by auto
qed

text ‹Connections between downsets, upsets and closure operators are outlined next.›

lemma preorder_clop: "clop (⇓::'a::preorder set ⇒ 'a set)"
  by (simp add: clop_def downset_set_ext downset_set_iso)

lemma clop_preorder_aux: "clop f ⟹ (x ∈ f {y} ⟷ f {x} ⊆ f {y})"
  by (simp add: clop_alt)

lemma clop_preorder: "clop f ⟹ class.preorder (λx y. f {x} ⊆ f {y}) (λx y. f {x} ⊂ f {y})"
  unfolding clop_def mono_def le_fun_def id_def comp_def by standard (auto simp: subset_not_subset_eq)

lemma preorder_clop_dual: "clop (⇑::'a::preorder_with_dual set ⇒ 'a set)"
  by (simp add: clop_def upset_set_anti upset_set_ext)

text ‹The closed elements of any closure operator over a complete lattice form an Inf-closed set (a Moore family).›

lemma clop_Inf_closed: 
  fixes f :: "'a::complete_lattice ⇒ 'a"
  shows  "clop f ⟹ Inf_closed_set (Fix f)" 
  unfolding clop_def Inf_closed_set_def mono_def le_fun_def comp_def id_def Fix_def
  by (smt (verit) Inf_greatest Inf_lower antisym mem_Collect_eq subsetCE)

lemma clop_top_Fix: 
  fixes f :: "'a::complete_lattice ⇒ 'a"
  shows  "clop f ⟹ ⊤ ∈ Fix f"
  by (simp add: clop_Fix_range clop_closure clop_top)


text ‹Conversely, every Inf-closed subset of a complete lattice is the set of fixpoints of some closure operator.›
 
lemma Inf_closed_clop: 
  fixes X :: "'a::complete_lattice set"
  shows "Inf_closed_set X ⟹ clop (λy. ⨅{x ∈ X. y ≤ x})"
  by (smt (verit) Collect_mono_iff Inf_superset_mono clop_alt dual_order.trans le_Inf_iff mem_Collect_eq)

lemma Inf_closed_clop_var: 
  fixes X :: "'a::complete_lattice set"
  shows "clop f ⟹ ∀x ∈ X. x ∈ range f ⟹ ⨅X ∈ range f"
  by (metis Inf_closed_set_def clop_Fix_range clop_Inf_closed subsetI)

text ‹It is well known that downsets and upsets over an ordering form subalgebras of the complete powerset lattice.›

typedef (overloaded) 'a downsets = "range (⇓::'a::order set ⇒ 'a set)"
  by fastforce

setup_lifting type_definition_downsets

typedef (overloaded) 'a upsets = "range (⇑::'a::order set ⇒ 'a set)"
  by fastforce

setup_lifting type_definition_upsets

instantiation downsets :: (order) Inf_lattice
begin

lift_definition Inf_downsets :: "'a downsets set ⇒ 'a downsets" is "Abs_downsets ∘ Inf ∘ (`) Rep_downsets".
  
lift_definition less_eq_downsets :: "'a downsets ⇒ 'a downsets ⇒ bool" is "λX Y. Rep_downsets X ⊆ Rep_downsets Y".

lift_definition less_downsets :: "'a downsets ⇒ 'a downsets ⇒ bool" is "λX Y. Rep_downsets X ⊂ Rep_downsets Y".

instance
  apply intro_classes 
      apply (transfer, simp)
     apply (transfer, blast)
    apply (simp add: Closure_Operators.less_eq_downsets.abs_eq Rep_downsets_inject)
   apply (transfer, smt (verit) Abs_downsets_inverse INF_lower Inf_closed_clop_var Rep_downsets image_iff o_def preorder_clop)
  apply (transfer, smt (verit) comp_def Abs_downsets_inverse Inf_closed_clop_var Rep_downsets image_iff le_INF_iff preorder_clop)
  done

end

instantiation upsets :: (order_with_dual) Inf_lattice
begin

lift_definition Inf_upsets :: "'a upsets set ⇒ 'a upsets" is "Abs_upsets ∘ Inf ∘ (`) Rep_upsets".
  
lift_definition less_eq_upsets :: "'a upsets ⇒ 'a upsets ⇒ bool" is "λX Y. Rep_upsets X ⊆ Rep_upsets Y".

lift_definition less_upsets :: "'a upsets ⇒ 'a upsets ⇒ bool" is "λX Y. Rep_upsets X ⊂ Rep_upsets Y".

instance
  apply intro_classes
      apply (transfer, simp)
     apply (transfer, blast)
    apply (simp add: Closure_Operators.less_eq_upsets.abs_eq Rep_upsets_inject)
   apply (transfer, smt (verit) Abs_upsets_inverse Inf_closed_clop_var Inf_lower Rep_upsets comp_apply image_iff preorder_clop_dual)
  apply (transfer, smt (verit) comp_def Abs_upsets_inverse Inf_closed_clop_var Inter_iff Rep_upsets image_iff preorder_clop_dual subsetCE subsetI)
  done

end

text ‹It has already been shown in the section on representations that the map ds, which maps elements of the order to its downset, is an order 
embedding. However, the duality between the underlying ordering and the lattices of up- and down-closed sets as categories can probably not be expressed, 
as there is no easy access to contravariant functors. ›


subsection ‹Co-Closure Operators›
                                
text ‹Next, the co-closure (or kernel) operation satisfies dual laws.›

definition coclop :: "('a::order ⇒ 'a::order) ⇒ bool" where
  "coclop f = (f ≤ id ∧ mono f ∧ f ≤ f ∘ f)"

lemma coclop_dual: "(coclop::('a::order_with_dual ⇒ 'a) ⇒ bool) = clop ∘ ∂⇩F"
  unfolding coclop_def clop_def id_def mono_def map_dual_def comp_def fun_eq_iff le_fun_def
  by (metis invol_dual_var ord_dual)

lemma coclop_dual_var: 
  fixes f :: "'a::order_with_dual ⇒ 'a"
  shows "coclop f = clop (∂⇩F f)"
  by (simp add: coclop_dual)

lemma clop_dual: "(clop::('a::order_with_dual ⇒ 'a) ⇒ bool) = coclop ∘ ∂⇩F"
  by (simp add: coclop_dual comp_assoc map_dual_invol)

lemma clop_dual_var: 
  fixes f :: "'a::order_with_dual ⇒ 'a"
  shows "clop f = coclop (∂⇩F f)"
  by (simp add: clop_dual)

lemma coclop_coextensive: "coclop f ⟹ f ≤ id"
  by (simp add: coclop_def)

lemma coclop_coextensive_var: "coclop f ⟹ f x ≤ x"
  using coclop_def le_funD by fastforce

lemma coclop_iso: "coclop f ⟹ mono f"
  by (simp add: coclop_def)

lemma coclop_iso_var: "coclop f ⟹ (x ≤ y ⟶ f x ≤ f y)"
  by (simp add: coclop_iso monoD)

lemma coclop_idem: "coclop f ⟹ f ∘ f = f"
  by (simp add: antisym coclop_def le_fun_def)

lemma coclop_closure: "coclop f ⟹ (x ∈ range f) = (f x = x)"
  by (simp add: coclop_idem retraction_prop)

lemma coclop_Fix_range: "coclop f ⟹ (Fix f = range f)"
  by (simp add: coclop_idem retraction_prop_fix)

lemma coclop_idem_var: "coclop f ⟹ f (f x) = f x"
  by (simp add: coclop_idem retraction_prop)

lemma coclop_Sup_closed_var: 
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'a"
  shows "coclop f ⟹ f ∘ Sup ∘ (`) f  = Sup ∘ (`) f"
  unfolding coclop_def mono_def comp_def le_fun_def 
  by (metis (mono_tags, lifting) SUP_le_iff antisym id_apply order_refl)

lemma Sup_closed_coclop_var: 
  fixes X :: "'a::complete_lattice set"
  shows "coclop f ⟹ ∀x ∈ X. x ∈ range f ⟹ ⨆X ∈ range f"
  by (smt (verit) Inf.INF_id_eq Sup.SUP_cong antisym coclop_closure coclop_coextensive_var coclop_iso id_apply mono_SUP)

lemma coclop_bot: 
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'a"
  shows "coclop f ⟹ f ⊥ = ⊥"
  by (simp add: bot.extremum_uniqueI coclop_coextensive_var)

lemma "coclop (f::'a::complete_lattice ⇒ 'a) ⟹ f (⨅x ∈ X. f x) = (⨅x ∈ X. f x)" (*nitpick*)
  oops

lemma "coclop (f::'a::complete_lattice ⇒ 'a) ⟹ f (f x ⊓ f y) = f x ⊓ f y" (*nitpick*)
  oops

lemma  "coclop (f::'a::complete_lattice ⇒ 'a) ⟹ f ⊤ = ⊤" (*nitpick*) 
  oops
  
lemma "coclop (f::'a set ⇒ 'a set) ⟹ f (⨅x ∈ X. f x) = (⨅x ∈ X. f x)" (*nitpick*)
  oops

lemma "coclop (f::'a set ⇒ 'a set) ⟹ f (f x ⊓ f y) = f x ⊓ f y" (*nitpick*)
  oops

lemma  "coclop (f::'a set ⇒ 'a set) ⟹ f ⊤ = ⊤" (*nitpick *)
  oops

lemma coclop_coclosure: "coclop f ⟹ f x = x ⟷ x ∈ range f"
 by (simp add: coclop_idem retraction_prop)
                                              
lemma coclop_coclosure_set: "coclop f ⟹ range f = Fix f"
  by (simp add: coclop_idem retraction_prop_fix)

lemma coclop_coclosure_prop: "(coclop::('a::complete_lattice ⇒ 'a) ⇒ bool) (Sup ∘ ↓)"
  by (simp add: coclop_def mono_def)

lemma coclop_coclosure_prop_var: "coclop (λx::'a::complete_lattice. ⨆{y. y ≤ x})"
  by (metis (mono_tags, lifting) Sup_atMost atMost_def coclop_def comp_apply eq_id_iff eq_refl mono_def)

lemma coclop_alt: "(coclop f) = (∀x y. f x ≤ y ⟷ f x ≤ f y)"
  unfolding coclop_def mono_def le_fun_def comp_def id_def
  by (meson dual_order.refl order_trans)

lemma coclop_adj: 
  fixes f :: "'a::order ⇒ 'b::order"
  shows "f ⊣ g ⟹ coclop (f ∘ g)"
  by (simp add: adj_cancel1 adj_idem1 adj_iso3 coclop_def)

text ‹Finally, a subset of a complete lattice is Sup-closed if and only if it is the set of fixpoints
of some co-closure operator.›

lemma coclop_Sup_closed: 
  fixes f :: "'a::complete_lattice ⇒ 'a"
  shows  "coclop f ⟹ Sup_closed_set (Fix f)"
  unfolding coclop_def Sup_closed_set_def mono_def le_fun_def comp_def id_def Fix_def
  by (smt (verit) Sup_least Sup_upper antisym_conv mem_Collect_eq subsetCE)

lemma Sup_closed_coclop: 
  fixes X :: "'a::complete_lattice set"
  shows "Sup_closed_set X ⟹ coclop (λy. ⨆{x ∈ X. x ≤ y})"
  unfolding Sup_closed_set_def coclop_def mono_def le_fun_def comp_def
  apply safe
  apply (metis (no_types, lifting) Sup_least eq_id_iff mem_Collect_eq)
  apply (smt (verit) Collect_mono_iff Sup_subset_mono dual_order.trans)
  by (simp add: Collect_mono_iff Sup_subset_mono Sup_upper)


subsection ‹Complete Lattices of Closed Elements›

text ‹The machinery developed allows showing that the closed elements in a complete
lattice (with respect to some closure operation) form themselves a complete lattice.›

class cl_op = ord +
  fixes cl_op :: "'a ⇒ 'a"
  assumes clop_ext: "x ≤ cl_op x"
  and clop_iso: "x ≤ y ⟹ cl_op x ≤ cl_op y"
  and clop_wtrans: "cl_op (cl_op x) ≤ cl_op x"

class clattice_with_clop = complete_lattice + cl_op

begin

lemma clop_cl_op: "clop cl_op"
  unfolding clop_def le_fun_def comp_def
  by (simp add: cl_op_class.clop_ext cl_op_class.clop_iso cl_op_class.clop_wtrans order_class.mono_def)

lemma clop_idem [simp]: "cl_op ∘ cl_op = cl_op"
  using clop_ext clop_wtrans order.antisym by auto

lemma clop_idem_var [simp]: "cl_op (cl_op x) = cl_op x"
  by (simp add: order.antisym clop_ext clop_wtrans)

lemma clop_range_Fix: "range cl_op = Fix cl_op"
  by (simp add: retraction_prop_fix)

lemma Inf_closed_cl_op_var: 
  fixes X :: "'a set"
  shows "∀x ∈ X. x ∈ range cl_op ⟹ ⨅X ∈ range cl_op"
proof-
  assume h: "∀x ∈ X. x ∈ range cl_op"
  hence "∀x ∈ X. cl_op x = x"
    by (simp add: retraction_prop)
  hence "cl_op (⨅X) = ⨅X"
    by (metis Inf_lower clop_ext clop_iso dual_order.antisym le_Inf_iff)
  thus ?thesis
    by (metis rangeI)
qed

lemma inf_closed_cl_op_var: "x ∈ range cl_op ⟹ y ∈ range cl_op ⟹ x ⊓ y ∈ range cl_op"
  by (smt (verit) Inf_closed_cl_op_var UnI1 insert_iff insert_is_Un inf_Inf)

end

typedef (overloaded) 'a::clattice_with_clop cl_op_im = "range (cl_op::'a ⇒ 'a)"
  by force

setup_lifting type_definition_cl_op_im

lemma cl_op_prop [iff]: "(cl_op (x ⊔ y) = cl_op y) = (cl_op (x::'a::clattice_with_clop) ≤ cl_op y)"
  by (smt (verit) cl_op_class.clop_iso clop_ext clop_wtrans inf_sup_ord(4) le_iff_sup sup.absorb_iff1 sup_left_commute)

lemma cl_op_prop_var [iff]: "(cl_op (x ⊔ cl_op y) = cl_op y) = (cl_op (x::'a::clattice_with_clop) ≤ cl_op y)"
  by (metis cl_op_prop clattice_with_clop_class.clop_idem_var)

instantiation cl_op_im :: (clattice_with_clop) complete_lattice
begin

lift_definition Inf_cl_op_im :: "'a cl_op_im set ⇒ 'a cl_op_im" is Inf
  by (simp add: Inf_closed_cl_op_var)
 
lift_definition Sup_cl_op_im :: "'a cl_op_im set ⇒ 'a cl_op_im" is "λX. cl_op (⨆X)"
  by simp

lift_definition inf_cl_op_im :: "'a cl_op_im ⇒ 'a cl_op_im ⇒ 'a cl_op_im" is inf
  by (simp add: inf_closed_cl_op_var)

lift_definition sup_cl_op_im :: "'a cl_op_im ⇒ 'a cl_op_im ⇒ 'a cl_op_im" is "λx y. cl_op (x ⊔ y)"
  by simp

lift_definition less_eq_cl_op_im :: "'a cl_op_im ⇒ 'a cl_op_im ⇒ bool" is "(≤)".

lift_definition less_cl_op_im :: "'a cl_op_im ⇒ 'a cl_op_im ⇒ bool" is "(<)".

lift_definition bot_cl_op_im :: "'a cl_op_im" is "cl_op ⊥"
  by simp

lift_definition top_cl_op_im :: "'a cl_op_im" is "⊤"
  by (simp add: clop_cl_op clop_closure clop_top)


instance
  apply (intro_classes; transfer)
                 apply (simp_all add: less_le_not_le Inf_lower Inf_greatest)
      apply (meson clop_cl_op clop_extensive_var dual_order.trans inf_sup_ord(3))
     apply (meson clop_cl_op clop_extensive_var dual_order.trans sup_ge2)
    apply (metis cl_op_class.clop_iso clop_cl_op clop_closure le_sup_iff)
   apply (meson Sup_upper clop_cl_op clop_extensive_var dual_order.trans)
  by (metis Sup_le_iff cl_op_class.clop_iso clop_cl_op clop_closure)

end

text ‹This statement is perhaps less useful as it might seem, because it is difficult to make it cooperate with concrete closure operators, 
which one would not generally like to define within a type class. Alternatively, a sublocale statement could perhaps be given. It would also 
have been nice to prove this statement for Sup-lattices---this would have cut down the number of proof obligations significantly.
But this would require a tighter integration of these structures. A similar statement could have been proved for co-closure operators. But this would
not lead to new insights.›

text ‹Next I show that for every surjective Sup-preserving function between complete lattices there is a closure operator 
such that the set of closed elements is isomorphic to the range of the surjection.›

lemma surj_Sup_pres_id:
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f" 
  shows "f ∘ (radj f) = id"
proof-
  have "f ⊣ (radj f)"
    using Sup_pres_ladj assms(2) radj_adj by auto
  thus ?thesis
    using adj_sur_inv assms(1) by blast
qed

lemma surj_Sup_pres_inj:
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f" 
  shows "inj (radj f)"
  by (metis assms comp_eq_dest_lhs id_apply injI surj_Sup_pres_id)

lemma surj_Sup_pres_inj_on: 
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f" 
  shows "inj_on f (range (radj f ∘ f))"
  by (smt (verit) Sup_pres_ladj_aux adj_idem2 assms(2) comp_apply inj_on_def retraction_prop)

lemma surj_Sup_pres_bij_on: 
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f" 
  shows "bij_betw f (range (radj f ∘ f)) UNIV"
  unfolding bij_betw_def
  apply safe
    apply (simp add: assms(1) assms(2) surj_Sup_pres_inj_on cong del: image_cong_simp)
   apply auto
  apply (metis (mono_tags) UNIV_I assms(1) assms(2) comp_apply id_apply image_image surj_Sup_pres_id surj_def)
  done

text ‹Thus the restriction of $f$ to the set of closed elements is indeed a bijection. The final fact
shows that it preserves Sups of closed elements, and hence is an isomorphism of complete lattices.›

lemma surj_Sup_pres_iso: 
  fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f" 
  shows "f ((radj f ∘ f) (⨆X)) = (⨆x ∈ X. f x)"
  by (metis assms(1) assms(2) comp_def pointfree_idE surj_Sup_pres_id)


subsection ‹A Quick Example: Dedekind-MacNeille Completions›

text ‹I only outline the basic construction. Additional facts about join density, and that the completion yields 
the least complete lattice that contains all Sups and Infs of the underlying posets, are left for future consideration.›

abbreviation "dm ≡ lb_set ∘ ub_set"

lemma up_set_prop: "(X::'a::preorder set) ≠ {} ⟹ ub_set X = ⋂{↑x |x. x ∈ X}"
  unfolding ub_set_def upset_def upset_set_def by (safe, simp_all, blast)

lemma lb_set_prop: "(X::'a::preorder set) ≠ {} ⟹ lb_set X = ⋂{↓x |x. x ∈ X}"
  unfolding lb_set_def downset_def downset_set_def by (safe, simp_all, blast)

lemma dm_downset_var: "dm {x} = ↓(x::'a::preorder)"
  unfolding lb_set_def ub_set_def downset_def downset_set_def 
  by (clarsimp, meson order_refl order_trans)

lemma dm_downset: "dm ∘ η = (↓::'a::preorder ⇒ 'a set)"
  using dm_downset_var fun.map_cong by fastforce

lemma dm_inj: "inj ((dm::'a::order set ⇒ 'a set) ∘ η)"
  by (simp add: dm_downset downset_inj)

lemma "clop (lb_set ∘ ub_set)"
  unfolding clop_def lb_set_def ub_set_def
  apply safe
  unfolding le_fun_def comp_def id_def mono_def
  by auto

end