Maximum and minimum of finite sets

max and min of finite sets

def Finset.max {α : Type u_2} [LinearOrder α] (s : Finset α) : WithBot α

Let s be a finset in a linear order. Then s.max is the maximum of s if s is not empty, and ⊥ otherwise. It belongs to WithBot α. If you want to get an element of α, see s.max'.

theorem Finset.max_eq_sup_coe {α : Type u_2} [LinearOrder α] {s : Finset α} : s.max = s.sup WithBot.some

theorem Finset.max_eq_sup_withBot {α : Type u_2} [LinearOrder α] (s : Finset α) : s.max = s.sup WithBot.some

@[simp]

theorem Finset.max_empty {α : Type u_2} [LinearOrder α] : ∅.max = ⊥

@[simp]

theorem Finset.max_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} : (insert a s).max = max (↑a) s.max

@[simp]

theorem Finset.max_singleton {α : Type u_2} [LinearOrder α] {a : α} : {a}.max = ↑a

theorem Finset.max_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a ∈ s) : ∃ (b : α), s.max = ↑b

theorem Finset.max_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) : ∃ (a : α), s.max = ↑a

theorem Finset.max_eq_bot {α : Type u_2} [LinearOrder α] {s : Finset α} : s.max = ⊥ ↔ s = ∅

theorem Finset.mem_of_max {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} : s.max = ↑a → a ∈ s

theorem Finset.le_max {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a ∈ s) : ↑a ≤ s.max

theorem Finset.notMem_of_max_lt_coe {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : s.max < ↑a) : a ∉ s

@[deprecated Finset.notMem_of_max_lt_coe (since := "2025-05-23")]

theorem Finset.not_mem_of_max_lt_coe {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : s.max < ↑a) : a ∉ s

Alias of Finset.notMem_of_max_lt_coe.

theorem Finset.le_max_of_eq {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : a ∈ s) (h₂ : s.max = ↑b) : a ≤ b

theorem Finset.notMem_of_max_lt {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = ↑b) : a ∉ s

@[deprecated Finset.notMem_of_max_lt (since := "2025-05-23")]

theorem Finset.not_mem_of_max_lt {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = ↑b) : a ∉ s

Alias of Finset.notMem_of_max_lt.

theorem Finset.max_union {α : Type u_2} [LinearOrder α] {s t : Finset α} : (s ∪ t).max = max s.max t.max

theorem Finset.max_mono {α : Type u_2} [LinearOrder α] {s t : Finset α} (st : s ⊆ t) : s.max ≤ t.max

theorem Finset.max_le {α : Type u_2} [LinearOrder α] {M : WithBot α} {s : Finset α} (st : ∀ a ∈ s, ↑a ≤ M) : s.max ≤ M

@[simp]

theorem Finset.max_le_iff {α : Type u_2} [LinearOrder α] {m : WithBot α} {s : Finset α} : s.max ≤ m ↔ ∀ a ∈ s, ↑a ≤ m

@[simp]

theorem Finset.max_eq_top {α : Type u_2} [LinearOrder α] [OrderTop α] {s : Finset α} : s.max = ⊤ ↔ ⊤ ∈ s

def Finset.min {α : Type u_2} [LinearOrder α] (s : Finset α) : WithTop α

Let s be a finset in a linear order. Then s.min is the minimum of s if s is not empty, and ⊤ otherwise. It belongs to WithTop α. If you want to get an element of α, see s.min'.

theorem Finset.min_eq_inf_withTop {α : Type u_2} [LinearOrder α] (s : Finset α) : s.min = s.inf WithTop.some

@[simp]

theorem Finset.min_empty {α : Type u_2} [LinearOrder α] : ∅.min = ⊤

@[simp]

theorem Finset.min_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} : (insert a s).min = min (↑a) s.min

@[simp]

theorem Finset.min_singleton {α : Type u_2} [LinearOrder α] {a : α} : {a}.min = ↑a

theorem Finset.min_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a ∈ s) : ∃ (b : α), s.min = ↑b

theorem Finset.min_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) : ∃ (a : α), s.min = ↑a

@[simp]

theorem Finset.min_eq_top {α : Type u_2} [LinearOrder α] {s : Finset α} : s.min = ⊤ ↔ s = ∅

theorem Finset.mem_of_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} : s.min = ↑a → a ∈ s

theorem Finset.min_le {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a ∈ s) : s.min ≤ ↑a

theorem Finset.notMem_of_coe_lt_min {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : ↑a < s.min) : a ∉ s

@[deprecated Finset.notMem_of_coe_lt_min (since := "2025-05-23")]

theorem Finset.not_mem_of_coe_lt_min {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : ↑a < s.min) : a ∉ s

Alias of Finset.notMem_of_coe_lt_min.

theorem Finset.min_le_of_eq {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : b ∈ s) (h₂ : s.min = ↑a) : a ≤ b

theorem Finset.notMem_of_lt_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = ↑b) : a ∉ s

@[deprecated Finset.notMem_of_lt_min (since := "2025-05-23")]

theorem Finset.not_mem_of_lt_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = ↑b) : a ∉ s

Alias of Finset.notMem_of_lt_min.

theorem Finset.min_union {α : Type u_2} [LinearOrder α] {s t : Finset α} : (s ∪ t).min = min s.min t.min

theorem Finset.min_mono {α : Type u_2} [LinearOrder α] {s t : Finset α} (st : s ⊆ t) : t.min ≤ s.min

theorem Finset.le_min {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} (st : ∀ a ∈ s, m ≤ ↑a) : m ≤ s.min

@[simp]

theorem Finset.le_min_iff {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} : m ≤ s.min ↔ ∀ a ∈ s, m ≤ ↑a

@[simp]

theorem Finset.min_eq_bot {α : Type u_2} [LinearOrder α] [OrderBot α] {s : Finset α} : s.min = ⊥ ↔ ⊥ ∈ s

def Finset.min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : α

Given a nonempty finset s in a linear order α, then s.min' H is its minimum, as an element of α, where H is a proof of nonemptiness. Without this assumption, use instead s.min, taking values in WithTop α.

def Finset.max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : α

Given a nonempty finset s in a linear order α, then s.max' H is its maximum, as an element of α, where H is a proof of nonemptiness. Without this assumption, use instead s.max, taking values in WithBot α.

theorem Finset.min'_mem {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.min' H ∈ s

theorem Finset.min'_le {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s) : s.min' ⋯ ≤ x

theorem Finset.le_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α) (H2 : ∀ y ∈ s, x ≤ y) : x ≤ s.min' H

theorem Finset.isLeast_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : IsLeast (↑s) (s.min' H)

@[simp]

theorem Finset.le_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y

@[simp]

theorem Finset.min'_singleton {α : Type u_2} [LinearOrder α] (a : α) : {a}.min' ⋯ = a

{a}.min' _ is a.

theorem Finset.max'_mem {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.max' H ∈ s

theorem Finset.le_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s) : x ≤ s.max' ⋯

theorem Finset.max'_le {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α) (H2 : ∀ y ∈ s, y ≤ x) : s.max' H ≤ x

theorem Finset.isGreatest_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : IsGreatest (↑s) (s.max' H)

@[simp]

theorem Finset.max'_le_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x

@[simp]

theorem Finset.max'_lt_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : s.max' H < x ↔ ∀ y ∈ s, y < x

@[simp]

theorem Finset.lt_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} : x < s.min' H ↔ ∀ y ∈ s, x < y

theorem Finset.max'_eq_sup' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.max' H = s.sup' H id

theorem Finset.min'_eq_inf' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) : s.min' H = s.inf' H id

@[simp]

theorem Finset.max'_singleton {α : Type u_2} [LinearOrder α] (a : α) : {a}.max' ⋯ = a

{a}.max' _ is a.

theorem Finset.min'_lt_max' {α : Type u_2} [LinearOrder α] (s : Finset α) {i j : α} (H1 : i ∈ s) (H2 : j ∈ s) (H3 : i ≠ j) : s.min' ⋯ < s.max' ⋯

theorem Finset.min'_lt_max'_of_card {α : Type u_2} [LinearOrder α] (s : Finset α) (h₂ : 1 < s.card) : s.min' ⋯ < s.max' ⋯

If there's more than 1 element, the min' is less than the max'. An alternate version of min'_lt_max' which is sometimes more convenient.

theorem Finset.max'_union {α : Type u_2} [LinearOrder α] {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) : (s₁ ∪ s₂).max' ⋯ = max (s₁.max' h₁) (s₂.max' h₂)

theorem Finset.min'_union {α : Type u_2} [LinearOrder α] {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) : (s₁ ∪ s₂).min' ⋯ = min (s₁.min' h₁) (s₂.min' h₂)

theorem Finset.map_ofDual_min {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) : WithTop.map (⇑OrderDual.ofDual) s.min = (image (⇑OrderDual.ofDual) s).max

theorem Finset.map_ofDual_max {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) : WithBot.map (⇑OrderDual.ofDual) s.max = (image (⇑OrderDual.ofDual) s).min

theorem Finset.map_toDual_min {α : Type u_2} [LinearOrder α] (s : Finset α) : WithTop.map (⇑OrderDual.toDual) s.min = (image (⇑OrderDual.toDual) s).max

theorem Finset.map_toDual_max {α : Type u_2} [LinearOrder α] (s : Finset α) : WithBot.map (⇑OrderDual.toDual) s.max = (image (⇑OrderDual.toDual) s).min

theorem Finset.ofDual_min' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) : OrderDual.ofDual (s.min' hs) = (image (⇑OrderDual.ofDual) s).max' ⋯

theorem Finset.ofDual_max' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) : OrderDual.ofDual (s.max' hs) = (image (⇑OrderDual.ofDual) s).min' ⋯

theorem Finset.toDual_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : OrderDual.toDual (s.min' hs) = (image (⇑OrderDual.toDual) s).max' ⋯

theorem Finset.toDual_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : OrderDual.toDual (s.max' hs) = (image (⇑OrderDual.toDual) s).min' ⋯

theorem Finset.max'_subset {α : Type u_2} [LinearOrder α] {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) : s.max' H ≤ t.max' ⋯

theorem Finset.min'_subset {α : Type u_2} [LinearOrder α] {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) : t.min' ⋯ ≤ s.min' H

theorem Finset.max'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) : (insert a s).max' ⋯ = max (s.max' H) a

theorem Finset.min'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) : (insert a s).min' ⋯ = min (s.min' H) a

theorem Finset.lt_max'_of_mem_erase_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.max' H)) : a < s.max' H

theorem Finset.min'_lt_of_mem_erase_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.min' H)) : s.min' H < a

@[simp]

theorem Finset.max'_image {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) (h : (image f s).Nonempty) : (image f s).max' h = f (s.max' ⋯)

To rewrite from right to left, use Monotone.map_finset_max'.

theorem Monotone.map_finset_max' {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) : f (s.max' h) = (Finset.image f s).max' ⋯

A version of Finset.max'_image with LHS and RHS reversed. Also, this version assumes that s is nonempty, not its image.

@[simp]

theorem Finset.min'_image {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) (h : (image f s).Nonempty) : (image f s).min' h = f (s.min' ⋯)

To rewrite from right to left, use Monotone.map_finset_min'.

theorem Monotone.map_finset_min' {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) : f (s.min' h) = (Finset.image f s).min' ⋯

A version of Finset.min'_image with LHS and RHS reversed. Also, this version assumes that s is nonempty, not its image.

theorem Finset.coe_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : ↑(s.max' hs) = s.max

theorem Finset.coe_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : ↑(s.min' hs) = s.min

theorem Finset.max_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : s.max ∈ image WithBot.some s

theorem Finset.min_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : s.min ∈ image WithTop.some s

theorem Finset.max_mem_insert_bot_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) : s.max ∈ insert ⊥ (image WithBot.some s)

theorem Finset.min_mem_insert_top_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) : s.min ∈ insert ⊤ (image WithTop.some s)

theorem Finset.max'_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).max' s0 ≠ x

theorem Finset.min'_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).min' s0 ≠ x

theorem Finset.max_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} : (s.erase x).max ≠ ↑x

theorem Finset.min_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} : (s.erase x).min ≠ ↑x

theorem Finset.exists_next_right {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) : ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z

theorem Finset.exists_next_left {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ∃ y ∈ s, y < x) : ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y

theorem Finset.card_le_of_interleaved {α : Type u_2} [LinearOrder α] {s t : Finset α} (h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) : s.card ≤ t.card + 1

If finsets s and t are interleaved, then Finset.card s ≤ Finset.card t + 1.

theorem Finset.card_le_diff_of_interleaved {α : Type u_2} [LinearOrder α] {s t : Finset α} (h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) : s.card ≤ (t \ s).card + 1

If finsets s and t are interleaved, then Finset.card s ≤ Finset.card (t \ s) + 1.

theorem Finset.induction_on_max {α : Type u_2} [LinearOrder α] [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅) (step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)) : p s

Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that:

• it is true on the empty Finset,
• for every s : Finset α and an element a strictly greater than all elements of s, p s implies p (insert a s).

theorem Finset.induction_on_min {α : Type u_2} [LinearOrder α] [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅) (step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, a < x) → p s → p (insert a s)) : p s

Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that:

• it is true on the empty Finset,
• for every s : Finset α and an element a strictly less than all elements of s, p s implies p (insert a s).

theorem Finset.induction_on_max_value {α : Type u_2} {ι : Type u_5} [LinearOrder α] [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅) (step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)) : p s

Induction principle for Finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : Finset α provided that:

• it is true on the empty Finset,
• for every s : Finset α and an element a such that for elements of s denoted by x we have f x ≤ f a, p s implies p (insert a s).

theorem Finset.induction_on_min_value {α : Type u_2} {ι : Type u_5} [LinearOrder α] [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅) (step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (insert a s)) : p s

Induction principle for Finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : Finset α provided that:

• it is true on the empty Finset,
• for every s : Finset α and an element a such that for elements of s denoted by x we have f a ≤ f x, p s implies p (insert a s).

theorem Finset.exists_max_image {α : Type u_2} {β : Type u_3} [LinearOrder α] (s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

theorem Finset.exists_min_image {α : Type u_2} {β : Type u_3} [LinearOrder α] (s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x'

theorem Finset.isGLB_iff_isLeast {α : Type u_2} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsGLB (↑s) i ↔ IsLeast (↑s) i

theorem Finset.isLUB_iff_isGreatest {α : Type u_2} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsLUB (↑s) i ↔ IsGreatest (↑s) i

theorem Finset.isGLB_mem {α : Type u_2} [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (↑s) i) (hs : s.Nonempty) : i ∈ s

theorem Finset.isLUB_mem {α : Type u_2} [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (↑s) i) (hs : s.Nonempty) : i ∈ s

theorem Multiset.exists_max_image {α : Type u_7} {R : Type u_8} [LinearOrder R] (f : α → R) {s : Multiset α} (hs : s ≠ 0) : ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

theorem Multiset.exists_min_image {α : Type u_7} {R : Type u_8} [LinearOrder R] (f : α → R) {s : Multiset α} (hs : s ≠ 0) : ∃ y ∈ s, ∀ z ∈ s, f y ≤ f z