# Order structures and monotonicity lemmas for `Set` #

source
theorem Set.monotoneOn_iff_monotone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} :
MonotoneOn f s ↔ Monotone fun (a : ↑s) => f ↑a
source
theorem Set.antitoneOn_iff_antitone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} :
AntitoneOn f s ↔ Antitone fun (a : ↑s) => f ↑a
source
theorem Set.strictMonoOn_iff_strictMono {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} :
StrictMonoOn f s ↔ StrictMono fun (a : ↑s) => f ↑a
source
theorem Set.strictAntiOn_iff_strictAnti {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} :
StrictAntiOn f s ↔ StrictAnti fun (a : ↑s) => f ↑a
source
theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le {α : Type u} {β : Type v} {s : Set α} [LinearOrder α] [LinearOrder β] {f : α → β} :
¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

source
theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt {α : Type u} {β : Type v} {s : Set α} [LinearOrder α] [LinearOrder β] {f : α → β} :
¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

### Monotone lemmas for sets #

source
theorem Monotone.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) :
Monotone fun (x : β) => f x ∩ g x
source
theorem MonotoneOn.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
MonotoneOn (fun (x : β) => f x ∩ g x) s
source
theorem Antitone.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) :
Antitone fun (x : β) => f x ∩ g x
source
theorem AntitoneOn.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
AntitoneOn (fun (x : β) => f x ∩ g x) s
source
theorem Monotone.union {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) :
Monotone fun (x : β) => f x ∪ g x
source
theorem MonotoneOn.union {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
MonotoneOn (fun (x : β) => f x ∪ g x) s
source
theorem Antitone.union {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) :
Antitone fun (x : β) => f x ∪ g x
source
theorem AntitoneOn.union {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
AntitoneOn (fun (x : β) => f x ∪ g x) s
source
theorem Set.monotone_setOf {α : Type u_1} {β : Type u_2} [Preorder α] {p : α → β → Prop} (hp : ∀ (b : β), Monotone fun (a : α) => p a b) :
Monotone fun (a : α) => {b : β | p a b}
source
theorem Set.antitone_setOf {α : Type u_1} {β : Type u_2} [Preorder α] {p : α → β → Prop} (hp : ∀ (b : β), Antitone fun (a : α) => p a b) :
Antitone fun (a : α) => {b : β | p a b}
source
theorem Set.antitone_bforall {α : Type u_1} {P : α → Prop} :
Antitone fun (s : Set α) => ∀ x ∈ s, P x

Quantifying over a set is antitone in the set