# Theory Minimum_Maximum

```section ‹Minimum and Maximum of Potentially Infinite Sets›

theory Minimum_Maximum
imports Main
begin

text ‹We define minima and maxima of sets. In contrast
to the existing @{const Min} and @{const Max} operators,
these operators are not restricted to finite sets ›

definition Maximum :: "'a :: linorder set ⇒ 'a" where
"Maximum S = (THE x. x ∈ S ∧ (∀ y ∈ S. y ≤ x))"
definition Minimum :: "'a :: linorder set ⇒ 'a" where
"Minimum S = (THE x. x ∈ S ∧ (∀ y ∈ S. x ≤ y))"

definition has_Maximum where "has_Maximum S = (∃ x. x ∈ S ∧ (∀ y ∈ S. y ≤ x))"
definition has_Minimum where "has_Minimum S = (∃ x. x ∈ S ∧ (∀ y ∈ S. x ≤ y))"

lemma eqMaximumI:
assumes "x ∈ S"
and "⋀ y. y ∈ S ⟹ y ≤ x"
shows "Maximum S = x"
unfolding Maximum_def
by (standard, insert assms, auto, fastforce)

lemma eqMinimumI:
assumes "x ∈ S"
and "⋀ y. y ∈ S ⟹ x ≤ y"
shows "Minimum S = x"
unfolding Minimum_def
by (standard, insert assms, auto, fastforce)

lemma has_MaximumD:
assumes "has_Maximum S"
shows "Maximum S ∈ S"
"x ∈ S ⟹ x ≤ Maximum S"
proof -
from assms[unfolded has_Maximum_def]
obtain m where *: "m ∈ S" "⋀ y. y ∈ S ⟹ y ≤ m" by auto
have id: "Maximum S = m"
by (rule eqMaximumI, insert *, auto)
from * id show "Maximum S ∈ S" "x ∈ S ⟹ x ≤ Maximum S" by auto
qed

lemma has_MinimumD:
assumes "has_Minimum S"
shows "Minimum S ∈ S"
"x ∈ S ⟹ Minimum S ≤ x"
proof -
from assms[unfolded has_Minimum_def]
obtain m where *: "m ∈ S" "⋀ y. y ∈ S ⟹ m ≤ y" by auto
have id: "Minimum S = m"
by (rule eqMinimumI, insert *, auto)
from * id show "Minimum S ∈ S" "x ∈ S ⟹ Minimum S ≤ x" by auto
qed

text ‹On non-empty finite sets, @{const Minimum} and @{const Min}
coincide, and similarly @{const Maximum} and @{const Max}.›

lemma Minimum_Min: assumes "finite S" "S ≠ {}"
shows "Minimum S = Min S"
by (rule eqMinimumI, insert assms, auto)

lemma Maximum_Max: assumes "finite S" "S ≠ {}"
shows "Maximum S = Max S"
by (rule eqMaximumI, insert assms, auto)

text ‹For natural numbers, having a maximum is the same as being bounded from above and non-empty,
or being finite and non-empty.›
lemma has_Maximum_nat_iff_bdd_above: "has_Maximum (A :: nat set) ⟷ bdd_above A ∧ A ≠ {}"
unfolding has_Maximum_def
by (metis bdd_above.I bdd_above_nat emptyE finite_has_maximal nat_le_linear)

lemma has_Maximum_nat_iff_finite: "has_Maximum (A :: nat set) ⟷ finite A ∧ A ≠ {}"
unfolding has_Maximum_nat_iff_bdd_above bdd_above_nat ..

lemma bdd_above_Maximum_nat: "(x :: nat) ∈ A ⟹ bdd_above A ⟹ x ≤ Maximum A"
by (rule has_MaximumD, auto simp: has_Maximum_nat_iff_bdd_above)

end```