Definitions

def minOn {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] (f : α → β) (x y : α) : α

Returns either x or y, the one with the smaller value under f.

If f x ≤ f y, it returns x, and otherwise returns y.

Equations

• minOn f x y = if f x ≤ f y then x else y

def maxOn {β : Type u_1} {α : Sort u_2} [i : LE β] [DecidableLE β] (f : α → β) (x y : α) : α

Returns either x or y, the one with the greater value under f.

If f y ≤ f x, it returns x, and otherwise returns y.

Equations

• maxOn f x y = minOn f x y

minOn Lemmas

theorem minOn_id {α : Type u_1} [Min α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] {x y : α} : minOn id x y = min x y

theorem maxOn_id {α : Type u_1} [Max α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] {x y : α} : maxOn id x y = max x y

theorem minOn_eq_or {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x y : α} : minOn f x y = x ∨ minOn f x y = y

@[simp]

theorem minOn_self {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x : α} : minOn f x x = x

theorem minOn_eq_left {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x y : α} (h : f x ≤ f y) : minOn f x y = x

theorem minOn_eq_right {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x y : α} (h : ¬f x ≤ f y) : minOn f x y = y

theorem minOn_eq_right_of_lt {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [LT β] [Std.Total fun (x1 x2 : β) => x1 ≤ x2] [Std.LawfulOrderLT β] {f : α → β} {x y : α} (h : f y < f x) : minOn f x y = y

theorem apply_minOn_le_left {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} : f (minOn f x y) ≤ f x

theorem apply_minOn_le_right {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} : f (minOn f x y) ≤ f y

theorem le_apply_minOn_iff {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} {b : β} : b ≤ f (minOn f x y) ↔ b ≤ f x ∧ b ≤ f y

theorem minOn_assoc {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y z : α} : minOn f (minOn f x y) z = minOn f x (minOn f y z)

instance instAssociativeMinOnOfIsLinearPreorder {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} : Std.Associative (minOn f)

theorem min_apply {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Min β] [Std.LawfulOrderLeftLeaningMin β] {f : α → β} {x y : α} : min (f x) (f y) = f (minOn f x y)

theorem minOn_eq_ite {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a b : α} : minOn f a b = if f a ≤ f b then a else b

@[deprecated minOn_eq_ite (since := "2026-07-21")]

theorem minOn_eq_if {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a b : α} : minOn f a b = if f a ≤ f b then a else b

theorem minOn_eq_min {α : Type u_1} {β : Type u_2} [Min α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] [LE β] [DecidableLE β] {f : α → β} {a b : α} (hf : f a ≤ f b ↔ a ≤ b) : minOn f a b = min a b

theorem min_apply_eq_min {α : Type u_1} {β : Type u_2} [LE α] [DecidableLE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [Min β] [LE β] [DecidableLE β] [Std.LawfulOrderLeftLeaningMin β] (f : α → β) {a b : α} (hf : f a ≤ f b ↔ a ≤ b) : min (f a) (f b) = f (min a b)

maxOn Lemmas

theorem maxOn_eq_minOn {β : Type u_1} {α : Sort u_2} [le : LE β] [DecidableLE β] {f : α → β} {x y : α} : maxOn f x y = minOn f x y

theorem maxOn_eq_or {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x y : α} : maxOn f x y = x ∨ maxOn f x y = y

@[simp]

theorem maxOn_self {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x : α} : maxOn f x x = x

theorem maxOn_eq_left {β : Type u_1} {α : Sort u_2} [le : LE β] [DecidableLE β] {f : α → β} {x y : α} (h : f y ≤ f x) : maxOn f x y = x

theorem maxOn_eq_right {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {x y : α} (h : ¬f y ≤ f x) : maxOn f x y = y

theorem maxOn_eq_right_of_lt {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [LT β] [Std.Total fun (x1 x2 : β) => x1 ≤ x2] [Std.LawfulOrderLT β] {f : α → β} {x y : α} (h : f x < f y) : maxOn f x y = y

theorem left_le_apply_maxOn {β : Type u_1} {α : Sort u_2} [le : LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} : f x ≤ f (maxOn f x y)

theorem right_le_apply_maxOn {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} : f y ≤ f (maxOn f x y)

theorem apply_maxOn_le_iff {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α} {b : β} : f (maxOn f x y) ≤ b ↔ f x ≤ b ∧ f y ≤ b

theorem maxOn_assoc {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y z : α} : maxOn f (maxOn f x y) z = maxOn f x (maxOn f y z)

instance instAssociativeMaxOnOfIsLinearPreorder {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} : Std.Associative (maxOn f)

theorem max_apply {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Max β] [Std.LawfulOrderLeftLeaningMax β] {f : α → β} {x y : α} : max (f x) (f y) = f (maxOn f x y)

theorem apply_maxOn {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] [Max β] [Std.LawfulOrderLeftLeaningMax β] {f : α → β} {x y : α} : f (maxOn f x y) = max (f x) (f y)

theorem maxOn_eq_ite {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a b : α} : maxOn f a b = if f b ≤ f a then a else b

@[deprecated maxOn_eq_ite (since := "2026-07-21")]

theorem maxOn_eq_if {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a b : α} : maxOn f a b = if f b ≤ f a then a else b

theorem maxOn_eq_max {α : Type u_1} {β : Type u_2} [Max α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] [LE β] [DecidableLE β] {f : α → β} {a b : α} (hf : f b ≤ f a ↔ b ≤ a) : maxOn f a b = max a b

theorem max_apply_eq_max {α : Type u_1} {β : Type u_2} [LE α] [DecidableLE α] [Max α] [Std.LawfulOrderLeftLeaningMax α] [Max β] [LE β] [DecidableLE β] [Std.LawfulOrderLeftLeaningMax β] (f : α → β) {a b : α} (hf : f b ≤ f a ↔ b ≤ a) : max (f a) (f b) = f (max a b)