Documentation

Mathlib.Data.Finset.Max

Maximum and minimum of finite sets #

max and min of finite sets #

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

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'.

Equations
theorem Finset.max_eq_sup_coe {α : Type u_2} [LinearOrder α] {s : Finset α} :
@[simp]
theorem Finset.max_empty {α : Type u_2} [LinearOrder α] :
@[simp]
theorem Finset.max_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} :
(insert a s).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 α} :
theorem Finset.mem_of_max {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} :
s.max = aa s
theorem Finset.le_max {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a s) :
a s.max
theorem Finset.not_mem_of_max_lt_coe {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : s.max < a) :
as
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.not_mem_of_max_lt {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = b) :
as
theorem Finset.max_union {α : Type u_2} [LinearOrder α] {s t : Finset α} :
(s t).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 : as, a M) :
s.max M
@[simp]
theorem Finset.max_le_iff {α : Type u_2} [LinearOrder α] {m : WithBot α} {s : Finset α} :
s.max m as, a m
@[simp]
theorem Finset.max_eq_top {α : Type u_2} [LinearOrder α] [OrderTop α] {s : Finset α} :
def Finset.min {α : Type u_2} [LinearOrder α] (s : Finset α) :

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'.

Equations
@[simp]
theorem Finset.min_empty {α : Type u_2} [LinearOrder α] :
@[simp]
theorem Finset.min_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} :
(insert a s).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 α} :
theorem Finset.mem_of_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} :
s.min = aa s
theorem Finset.min_le {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a s) :
s.min a
theorem Finset.not_mem_of_coe_lt_min {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : a < s.min) :
as
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.not_mem_of_lt_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = b) :
as
theorem Finset.min_union {α : Type u_2} [LinearOrder α] {s t : Finset α} :
(s t).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 : as, m a) :
m s.min
@[simp]
theorem Finset.le_min_iff {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} :
m s.min as, m a
@[simp]
theorem Finset.min_eq_bot {α : Type u_2} [LinearOrder α] [OrderBot α] {s : Finset α} :
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 α.

Equations
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 α.

Equations
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 : ys, 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 ys, 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 : ys, 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 ys, y x
@[simp]
theorem Finset.max'_lt_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :
s.max' H < x ys, y < x
@[simp]
theorem Finset.lt_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :
x < s.min' H ys, 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' = 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' = s₁.min' h₁ s₂.min' h₂
theorem Finset.ofDual_min' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) :
theorem Finset.ofDual_max' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) :
theorem Finset.toDual_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
theorem Finset.toDual_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
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' = s.max' H a
theorem Finset.min'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) :
(insert a s).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) :
theorem Finset.min_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
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 : ys, x < y) :
ys, x < y zs, x < zy z
theorem Finset.exists_next_left {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ys, y < x) :
ys, y < x zs, z < xz y
theorem Finset.card_le_of_interleaved {α : Type u_2} [LinearOrder α] {s t : Finset α} (h : xs, ys, x < y(∀ zs, zSet.Ioo x y)zt, 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 : xs, ys, x < y(∀ zs, zSet.Ioo x y)zt, 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 α), (∀ xs, x < a)p sp (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 α), (∀ xs, a < x)p sp (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 ι), as(∀ xs, f x f a)p sp (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 ι), as(∀ xs, f a f x)p sp (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) :
xs, x's, f x' f x
theorem Finset.exists_min_image {α : Type u_2} {β : Type u_3} [LinearOrder α] (s : Finset β) (f : βα) (h : s.Nonempty) :
xs, 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