max
and min
#
This file proves basic properties about maxima and minima on a LinearOrder
.
Tags #
min, max
An instance asserting that max a a = a
An instance asserting that min a a = a
theorem
MonotoneOn.map_max
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{s : Set α}
{a b : α}
(hf : MonotoneOn f s)
(ha : a ∈ s)
(hb : b ∈ s)
:
theorem
MonotoneOn.map_min
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{s : Set α}
{a b : α}
(hf : MonotoneOn f s)
(ha : a ∈ s)
(hb : b ∈ s)
:
theorem
AntitoneOn.map_max
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{s : Set α}
{a b : α}
(hf : AntitoneOn f s)
(ha : a ∈ s)
(hb : b ∈ s)
:
theorem
AntitoneOn.map_min
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{s : Set α}
{a b : α}
(hf : AntitoneOn f s)
(ha : a ∈ s)
(hb : b ∈ s)
:
theorem
Monotone.map_max
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{a b : α}
(hf : Monotone f)
:
theorem
Monotone.map_min
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{a b : α}
(hf : Monotone f)
:
theorem
Antitone.map_max
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{a b : α}
(hf : Antitone f)
:
theorem
Antitone.map_min
{α : Type u}
{β : Type v}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
{a b : α}
(hf : Antitone f)
: