Order structures and monotonicity lemmas for Set

theorem Set.monotoneOn_iff_monotone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : MonotoneOn f s ↔ Monotone fun (a : ↑s) => f ↑a

theorem Set.antitoneOn_iff_antitone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : AntitoneOn f s ↔ Antitone fun (a : ↑s) => f ↑a

theorem Set.strictMonoOn_iff_strictMono {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : StrictMonoOn f s ↔ StrictMono fun (a : ↑s) => f ↑a

theorem Set.strictAntiOn_iff_strictAnti {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : StrictAntiOn f s ↔ StrictAnti fun (a : ↑s) => f ↑a

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 : α), a ∈ s ∧ ∃ (b : α), b ∈ s ∧ ∃ (c : α), 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.

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 : α), a ∈ s ∧ ∃ (b : α), b ∈ s ∧ ∃ (c : α), 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

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

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

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

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

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

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

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

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

theorem Set.monotone_ofPred {α : Type u_1} {β : Type u_2} [Preorder α] {p : α → β → Prop} (hp : ∀ (b : β), Monotone fun (a : α) => p a b) : Monotone fun (a : α) => {b : β | p a b}

@[deprecated Set.monotone_ofPred (since := "2026-07-09")]

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}

Alias of Set.monotone_ofPred.

theorem Set.antitone_ofPred {α : Type u_1} {β : Type u_2} [Preorder α] {p : α → β → Prop} (hp : ∀ (b : β), Antitone fun (a : α) => p a b) : Antitone fun (a : α) => {b : β | p a b}

@[deprecated Set.antitone_ofPred (since := "2026-07-09")]

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}

Alias of Set.antitone_ofPred.

theorem Set.antitone_bforall {α : Type u_1} {P : α → Prop} : Antitone fun (s : Set α) => ∀ (x : α), x ∈ s → P x

Quantifying over a set is antitone in the set