--- 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)