diff -r 62c039ce397c -r b1af763166f4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Feb 25 14:23:25 2025 +0100
+++ b/src/HOL/Fun.thy	Tue Feb 25 15:54:41 2025 +0100
@@ -1339,6 +1339,26 @@
   for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   by (auto simp add: mono_def intro: Lattices.sup_least)
 
+lemma monotone_on_sup_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_sup"
+  shows "monotone_on A P (\<le>) f \<Longrightarrow> monotone_on A P (\<le>) g \<Longrightarrow> monotone_on A P (\<le>) (f \<squnion> g)"
+  by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)
+
+lemma monotone_on_inf_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_inf"
+  shows "monotone_on A P (\<le>) f \<Longrightarrow> monotone_on A P (\<le>) g \<Longrightarrow> monotone_on A P (\<le>) (f \<sqinter> g)"
+  by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)
+
+lemma antimonotone_on_sup_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_sup"
+  shows "monotone_on A P (\<ge>) f \<Longrightarrow> monotone_on A P (\<ge>) g \<Longrightarrow> monotone_on A P (\<ge>) (f \<squnion> g)"
+  by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)
+
+lemma antimonotone_on_inf_fun:
+  fixes f g :: "_ \<Rightarrow> _:: semilattice_inf"
+  shows "monotone_on A P (\<ge>) f \<Longrightarrow> monotone_on A P (\<ge>) g \<Longrightarrow> monotone_on A P (\<ge>) (f \<sqinter> g)"
+  by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)
+
 lemma (in linorder) min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
   by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)