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

s.max = s.sup WithBot.some

Instances For

source

theorem Finset.max_eq_sup_coe {α : Type u_2} [LinearOrder α] {s : Finset α} :

s.max = s.sup WithBot.some

source

theorem Finset.max_eq_sup_withBot {α : Type u_2} [LinearOrder α] (s : Finset α) :

s.max = s.sup WithBot.some

source

@[simp]

theorem Finset.max_empty {α : Type u_2} [LinearOrder α] :

∅.max = ⊥

source

@[simp]

theorem Finset.max_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} :

(insert a s).max = ↑a ⊔ s.max

source

@[simp]

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

{a}.max = ↑a

source

theorem Finset.max_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a ∈ s) :

∃ (b : α), s.max = ↑b

source

theorem Finset.max_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) :

∃ (a : α), s.max = ↑a

source

theorem Finset.max_eq_bot {α : Type u_2} [LinearOrder α] {s : Finset α} :

s.max = ⊥ ↔ s = ∅

source

theorem Finset.mem_of_max {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} :

s.max = ↑a → a ∈ s

source

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

↑a ≤ s.max

source

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

a ∉ s

source

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

a ≤ b

source

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

a ∉ s

source

theorem Finset.max_union {α : Type u_2} [LinearOrder α] {s t : Finset α} :

(s ∪ t).max = s.max ⊔ t.max

source

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

s.max ≤ t.max

source

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

s.max ≤ M

source

@[simp]

theorem Finset.max_le_iff {α : Type u_2} [LinearOrder α] {m : WithBot α} {s : Finset α} :

s.max ≤ m ↔ ∀ a ∈ s, ↑a ≤ m

source

@[simp]

theorem Finset.max_eq_top {α : Type u_2} [LinearOrder α] [OrderTop α] {s : Finset α} :

s.max = ⊤ ↔ ⊤ ∈ s

source

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

Equations

s.min = s.inf WithTop.some

Instances For

source

theorem Finset.min_eq_inf_withTop {α : Type u_2} [LinearOrder α] (s : Finset α) :

s.min = s.inf WithTop.some

source

@[simp]

theorem Finset.min_empty {α : Type u_2} [LinearOrder α] :

∅.min = ⊤

source

@[simp]

theorem Finset.min_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} :

(insert a s).min = ↑a ⊓ s.min

source

@[simp]

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

{a}.min = ↑a

source

theorem Finset.min_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a ∈ s) :

∃ (b : α), s.min = ↑b

source

theorem Finset.min_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) :

∃ (a : α), s.min = ↑a

source

@[simp]

theorem Finset.min_eq_top {α : Type u_2} [LinearOrder α] {s : Finset α} :

s.min = ⊤ ↔ s = ∅

source

theorem Finset.mem_of_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} :

s.min = ↑a → a ∈ s

source

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

s.min ≤ ↑a

source

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

a ∉ s

source

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

a ≤ b

source

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

a ∉ s

source

theorem Finset.min_union {α : Type u_2} [LinearOrder α] {s t : Finset α} :

(s ∪ t).min = s.min ⊓ t.min

source

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

t.min ≤ s.min

source

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

m ≤ s.min

source

@[simp]

theorem Finset.le_min_iff {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} :

m ≤ s.min ↔ ∀ a ∈ s, m ≤ ↑a

source

@[simp]

theorem Finset.min_eq_bot {α : Type u_2} [LinearOrder α] [OrderBot α] {s : Finset α} :

s.min = ⊥ ↔ ⊥ ∈ s

source

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

s.min' H = s.inf' H id

Instances For

source

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

s.max' H = s.sup' H id

Instances For

source

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

s.min' H ∈ s

source

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

s.min' ⋯ ≤ x

source

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

x ≤ s.min' H

source

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

IsLeast (↑s) (s.min' H)

source

@[simp]

theorem Finset.le_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :

x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y

source

@[simp]

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

{a}.min' ⋯ = a

{a}.min' _ is a.

source

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

s.max' H ∈ s

source

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

x ≤ s.max' ⋯

source

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

s.max' H ≤ x

source

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

IsGreatest (↑s) (s.max' H)

source

@[simp]

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

s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x

source

@[simp]

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

s.max' H < x ↔ ∀ y ∈ s, y < x

source

@[simp]

theorem Finset.lt_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :

x < s.min' H ↔ ∀ y ∈ s, x < y

source

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

s.max' H = s.sup' H id

source

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

s.min' H = s.inf' H id

source

@[simp]

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

{a}.max' ⋯ = a

{a}.max' _ is a.

source

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

source

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.

source

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₂

source

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₂

source

theorem Finset.map_ofDual_min {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) :

WithTop.map (⇑OrderDual.ofDual) s.min = (Finset.image (⇑OrderDual.ofDual) s).max

source

theorem Finset.map_ofDual_max {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) :

WithBot.map (⇑OrderDual.ofDual) s.max = (Finset.image (⇑OrderDual.ofDual) s).min

source

theorem Finset.map_toDual_min {α : Type u_2} [LinearOrder α] (s : Finset α) :

WithTop.map (⇑OrderDual.toDual) s.min = (Finset.image (⇑OrderDual.toDual) s).max

source

theorem Finset.map_toDual_max {α : Type u_2} [LinearOrder α] (s : Finset α) :

WithBot.map (⇑OrderDual.toDual) s.max = (Finset.image (⇑OrderDual.toDual) s).min

source

theorem Finset.ofDual_min' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) :

OrderDual.ofDual (s.min' hs) = (Finset.image (⇑OrderDual.ofDual) s).max' ⋯

source

theorem Finset.ofDual_max' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) :

OrderDual.ofDual (s.max' hs) = (Finset.image (⇑OrderDual.ofDual) s).min' ⋯

source

theorem Finset.toDual_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :

OrderDual.toDual (s.min' hs) = (Finset.image (⇑OrderDual.toDual) s).max' ⋯

source

theorem Finset.toDual_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :

OrderDual.toDual (s.max' hs) = (Finset.image (⇑OrderDual.toDual) s).min' ⋯

source

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

s.max' H ≤ t.max' ⋯

source

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

t.min' ⋯ ≤ s.min' H

source

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

(insert a s).max' ⋯ = s.max' H ⊔ a

source

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

(insert a s).min' ⋯ = s.min' H ⊓ a

source

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

source

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

source

@[simp]

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

(Finset.image f s).max' h = f (s.max' ⋯)

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

source

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.

source

@[simp]

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

(Finset.image f s).min' h = f (s.min' ⋯)

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

source

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.

source

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

↑(s.max' hs) = s.max

source

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

↑(s.min' hs) = s.min

source

theorem Finset.max_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :

s.max ∈ Finset.image WithBot.some s

source

theorem Finset.min_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :

s.min ∈ Finset.image WithTop.some s

source

theorem Finset.max_mem_insert_bot_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) :

s.max ∈ insert ⊥ (Finset.image WithBot.some s)

source

theorem Finset.min_mem_insert_top_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) :

s.min ∈ insert ⊤ (Finset.image WithTop.some s)

source

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

(s.erase x).max' s0 ≠ x

source

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

(s.erase x).min' s0 ≠ x

source

theorem Finset.max_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} :

(s.erase x).max ≠ ↑x

source

theorem Finset.min_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} :

(s.erase x).min ≠ ↑x

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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

source

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'

source

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

IsGLB (↑s) i ↔ IsLeast (↑s) i

source

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

IsLUB (↑s) i ↔ IsGreatest (↑s) i

source

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

i ∈ s

source

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

i ∈ s

Documentation

Mathlib.Data.Finset.Max

Maximum and minimum of finite sets #

max and min of finite sets #