Mathlib.Data.Finset.Max

Finset.max definition

(s : Finset α) : WithBot α

Full source

/-- 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'`. -/
protected def max (s : Finset α) : WithBot α :=
  sup s (↑)

Maximum of a finite set in a linear order

Informal description

Given a finite set $s$ in a linearly ordered type $\alpha$, the maximum element of $s$ is defined as the supremum of the set when viewed in `WithBot α` (which adds a bottom element $\bot$ to $\alpha$). If $s$ is nonempty, this returns the actual maximum element of $s$; otherwise, it returns $\bot$.

Finset.max_eq_sup_coe theorem

{s : Finset α} : s.max = s.sup (↑)

Full source

theorem max_eq_sup_coe {s : Finset α} : s.max = s.sup (↑) :=
  rfl

Maximum as Supremum Under Canonical Embedding

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the maximum element of $s$ (viewed in `WithBot α`) is equal to the supremum of the image of $s$ under the canonical embedding of $\alpha$ into `WithBot α$.

Finset.max_eq_sup_withBot theorem

(s : Finset α) : s.max = sup s (↑)

Full source

theorem max_eq_sup_withBot (s : Finset α) : s.max = sup s (↑) :=
  rfl

Maximum of Finite Set Equals Supremum Under Canonical Embedding

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the maximum element of $s$ (viewed in `WithBot α`) is equal to the supremum of the image of $s$ under the canonical embedding $\alpha \hookrightarrow \text{WithBot }\alpha$.

Finset.max_empty theorem

: (∅ : Finset α).max = ⊥

Full source

@[simp]
theorem max_empty : (∅ : Finset α).max = ⊥ :=
  rfl

Maximum of Empty Set is Bottom Element

Informal description

For any linearly ordered type $\alpha$, the maximum element of the empty finite set is the bottom element $\bot$ in `WithBot α$.

Finset.max_insert theorem

{a : α} {s : Finset α} : (insert a s).max = max (↑a) s.max

Full source

@[simp]
theorem max_insert {a : α} {s : Finset α} : (insert a s).max = max ↑a s.max :=
  fold_insert_idem

Insertion Preserves Maximum in Finite Sets: $\max(\{a\} \cup s) = \max(a, \max(s))$

Informal description

For any element $a$ in a linearly ordered type $\alpha$ and any finite set $s \subseteq \alpha$, the maximum element of the set $\{a\} \cup s$ is equal to the maximum of $a$ and the maximum element of $s$ (where both are viewed in $\text{WithBot }\alpha$). That is, \[ \max(\{a\} \cup s) = \max(a, \max(s)). \]

Finset.max_singleton theorem

{a : α} : Finset.max { a } = (a : WithBot α)

Full source

@[simp]
theorem max_singleton {a : α} : Finset.max {a} = (a : WithBot α) := by
  rw [← insert_empty_eq]
  exact max_insert

Maximum of Singleton Set is the Element Itself

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the maximum element of the singleton set $\{a\}$ is $a$ (viewed as an element of $\text{WithBot }\alpha$).

Finset.max_of_mem theorem

{s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.max = b

Full source

theorem max_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.max = b := by
  obtain ⟨b, h, _⟩ := le_sup (α := WithBot α) h _ rfl
  exact ⟨b, h⟩

Existence of Maximum Element for Nonempty Finite Sets in Linear Order

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any element $a \in s$, there exists an element $b \in \alpha$ such that the maximum element of $s$ (viewed in `WithBot α`) is equal to $b$.

Finset.max_of_nonempty theorem

{s : Finset α} (h : s.Nonempty) : ∃ a : α, s.max = a

Full source

theorem max_of_nonempty {s : Finset α} (h : s.Nonempty) : ∃ a : α, s.max = a :=
  let ⟨_, h⟩ := h
  max_of_mem h

Existence of Maximum Element for Nonempty Finite Sets in Linear Order

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, there exists an element $a \in \alpha$ such that the maximum element of $s$ is equal to $a$.

Finset.max_eq_bot theorem

{s : Finset α} : s.max = ⊥ ↔ s = ∅

Full source

theorem max_eq_bot {s : Finset α} : s.max = ⊥ ↔ s = ∅ :=
  ⟨fun h ↦ s.eq_empty_or_nonempty.elim id fun H ↦ by
      obtain ⟨a, ha⟩ := max_of_nonempty H
      rw [h] at ha; cases ha; , -- the `;` is needed since the `cases` syntax allows `cases a, b`
    fun h ↦ h.symm ▸ max_empty⟩

Maximum of Finite Set is Bottom if and only if Set is Empty

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the maximum element of $s$ is equal to the bottom element $\bot$ in `WithBot α` if and only if $s$ is the empty set.

Finset.mem_of_max theorem

{s : Finset α} : ∀ {a : α}, s.max = a → a ∈ s

Full source

theorem mem_of_max {s : Finset α} : ∀ {a : α}, s.max = a → a ∈ s := by
  induction' s using Finset.induction_on with b s _ ih
  · intro _ H; cases H
  · intro a h
    by_cases p : b = a
    · induction p
      exact mem_insert_self b s
    · rcases max_choice (↑b) s.max with q | q <;> rw [max_insert, q] at h
      · cases h
        cases p rfl
      · exact mem_insert_of_mem (ih h)

Maximum Element Belongs to Finite Set: $\max(s) = a \implies a \in s$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any element $a \in \alpha$, if the maximum element of $s$ is equal to $a$, then $a$ belongs to $s$.

Finset.le_max theorem

{a : α} {s : Finset α} (as : a ∈ s) : ↑a ≤ s.max

Full source

theorem le_max {a : α} {s : Finset α} (as : a ∈ s) : ↑a ≤ s.max :=
  le_sup as

Element in Finite Set is Bounded by Maximum: $a \leq \max(s)$ for $a \in s$

Informal description

For any element $a$ in a finite set $s$ of a linearly ordered type $\alpha$, the element $a$ is less than or equal to the maximum element of $s$ (when viewed in `WithBot α`), i.e., $a \leq \max(s)$.

Finset.not_mem_of_max_lt_coe theorem

{a : α} {s : Finset α} (h : s.max < a) : a ∉ s

Full source

theorem not_mem_of_max_lt_coe {a : α} {s : Finset α} (h : s.max < a) : a ∉ s :=
  mt le_max h.not_le

Non-membership from Maximum Inequality: $\max(s) < a \implies a \notin s$

Informal description

For any element $a$ in a linearly ordered type $\alpha$ and any finite set $s$ of $\alpha$, if the maximum element of $s$ (viewed in `WithBot α`) is strictly less than $a$, then $a$ does not belong to $s$.

Finset.le_max_of_eq theorem

{s : Finset α} {a b : α} (h₁ : a ∈ s) (h₂ : s.max = b) : a ≤ b

Full source

theorem le_max_of_eq {s : Finset α} {a b : α} (h₁ : a ∈ s) (h₂ : s.max = b) : a ≤ b :=
  WithBot.coe_le_coe.mp <| (le_max h₁).trans h₂.le

Element in Finite Set is Bounded by its Maximum: $a \leq \max(s)$ when $\max(s) = b$ and $a \in s$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any elements $a, b \in \alpha$, if $a$ belongs to $s$ and the maximum element of $s$ is equal to $b$, then $a \leq b$.

Finset.not_mem_of_max_lt theorem

{s : Finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = ↑b) : a ∉ s

Full source

theorem not_mem_of_max_lt {s : Finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = ↑b) : a ∉ s :=
  Finset.not_mem_of_max_lt_coe <| h₂.trans_lt <| WithBot.coe_lt_coe.mpr h₁

Non-membership from Maximum Inequality: $b < a \land \max(s) = b \implies a \notin s$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any elements $a, b \in \alpha$, if $b < a$ and the maximum element of $s$ is equal to $b$ (when viewed in `WithBot α`), then $a$ does not belong to $s$.

Finset.max_union theorem

{s t : Finset α} : (s ∪ t).max = s.max ⊔ t.max

Full source

theorem max_union {s t : Finset α} : (s ∪ t).max = s.max ⊔ t.max := sup_union

Maximum of Union Equals Join of Maxima for Finite Sets

Informal description

For any two finite sets $s$ and $t$ in a linearly ordered type $\alpha$, the maximum element of their union $s \cup t$ is equal to the supremum (join) of the maximum elements of $s$ and $t$ in `WithBot α`. That is, \[ \max(s \cup t) = \max(s) \sqcup \max(t). \]

Finset.max_mono theorem

{s t : Finset α} (st : s ⊆ t) : s.max ≤ t.max

Full source

@[gcongr]
theorem max_mono {s t : Finset α} (st : s ⊆ t) : s.max ≤ t.max :=
  sup_mono st

Monotonicity of Maximum under Subset Inclusion: $s \subseteq t \Rightarrow \max s \leq \max t$

Informal description

For any two finite sets $s$ and $t$ in a linearly ordered type $\alpha$, if $s$ is a subset of $t$, then the maximum element of $s$ is less than or equal to the maximum element of $t$ (where both maxima are considered in $\text{WithBot}\ \alpha$).

Finset.max_le theorem

{M : WithBot α} {s : Finset α} (st : ∀ a ∈ s, (a : WithBot α) ≤ M) : s.max ≤ M

Full source

protected theorem max_le {M : WithBot α} {s : Finset α} (st : ∀ a ∈ s, (a : WithBot α) ≤ M) :
    s.max ≤ M :=
  Finset.sup_le st

Maximum of Finite Set is Bounded by Common Upper Bound

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any upper bound $M$ (in `WithBot α`), if every element $a \in s$ satisfies $a \leq M$, then the maximum element of $s$ is also bounded above by $M$, i.e., $\max(s) \leq M$.

Finset.max_le_iff theorem

{m : WithBot α} {s : Finset α} : s.max ≤ m ↔ ∀ a ∈ s, a ≤ m

Full source

@[simp]
protected lemma max_le_iff {m : WithBot α} {s : Finset α} : s.max ≤ m ↔ ∀ a ∈ s, a ≤ m :=
  Finset.sup_le_iff

Maximum Element of Finite Set is Least Upper Bound: $\max s \leq m \leftrightarrow \forall a \in s, a \leq m$

Informal description

For a finite set $s$ in a linearly ordered type $\alpha$ and an element $m$ in $\text{WithBot}\ \alpha$, the maximum element of $s$ is less than or equal to $m$ if and only if every element $a \in s$ satisfies $a \leq m$.

Finset.max_eq_top theorem

[OrderTop α] {s : Finset α} : s.max = ⊤ ↔ ⊤ ∈ s

Full source

@[simp]
protected lemma max_eq_top [OrderTop α] {s : Finset α} : s.max = ⊤ ↔ ⊤ ∈ s :=
  Finset.sup_eq_top_iff.trans <| by simp

Maximum of Finite Set Equals Top Element if and only if Top is in Set

Informal description

For a finite set $s$ in a linearly ordered type $\alpha$ with a top element $\top$, the maximum element of $s$ equals $\top$ if and only if $\top$ is an element of $s$.

Finset.min definition

(s : Finset α) : WithTop α

Full source

/-- 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'`. -/
protected def min (s : Finset α) : WithTop α :=
  inf s (↑)

Minimum of a finite set in a linear order

Informal description

For a finite set $s$ in a linearly ordered type $\alpha$, the minimum $\min s$ is defined as the smallest element of $s$ if $s$ is nonempty, and $\top$ (the top element) otherwise. The result is an element of $\text{WithTop}\ \alpha$. To obtain an element of $\alpha$ directly, use `s.min'`.

Finset.min_eq_inf_withTop theorem

(s : Finset α) : s.min = inf s (↑)

Full source

theorem min_eq_inf_withTop (s : Finset α) : s.min = inf s (↑) :=
  rfl

Minimum as Infimum in $\text{WithTop}\ \alpha$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the minimum element of $s$ (considered as an element of $\text{WithTop}\ \alpha$) is equal to the infimum of the set $s$ under the canonical injection from $\alpha$ to $\text{WithTop}\ \alpha$. More precisely, if $s = \{a_1, \dots, a_n\}$, then $\min s = \inf \{\text{some}\ a_1, \dots, \text{some}\ a_n\}$ in $\text{WithTop}\ \alpha$, where $\text{some}\ a_i$ denotes the injection of $a_i$ into $\text{WithTop}\ \alpha$.

Finset.min_empty theorem

: (∅ : Finset α).min = ⊤

Full source

@[simp]
theorem min_empty : (∅ : Finset α).min = ⊤ :=
  rfl

Minimum of Empty Set is Top Element

Informal description

For any type $\alpha$ with a linear order, the minimum of the empty finite set $\emptyset$ is equal to the top element $\top$ of $\text{WithTop}\ \alpha$.

Finset.min_insert theorem

{a : α} {s : Finset α} : (insert a s).min = min (↑a) s.min

Full source

@[simp]
theorem min_insert {a : α} {s : Finset α} : (insert a s).min = min (↑a) s.min :=
  fold_insert_idem

Minimum of Inserted Element in Finite Set: $\min(\{a\} \cup s) = \min(a, \min s)$

Informal description

For any element $a$ of a linearly ordered type $\alpha$ and any finite set $s$ of elements of $\alpha$, the minimum of the set $\{a\} \cup s$ is equal to the minimum of $a$ and the minimum of $s$ (where both minima are considered in $\text{WithTop}\ \alpha$).

Finset.min_singleton theorem

{a : α} : Finset.min { a } = (a : WithTop α)

Full source

@[simp]
theorem min_singleton {a : α} : Finset.min {a} = (a : WithTop α) := by
  rw [← insert_empty_eq]
  exact min_insert

Minimum of Singleton Set: $\min\{a\} = a$

Informal description

For any element $a$ of a linearly ordered type $\alpha$, the minimum of the singleton set $\{a\}$ is equal to $a$ (considered as an element of $\text{WithTop}\ \alpha$).

Finset.min_of_mem theorem

{s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.min = b

Full source

theorem min_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.min = b := by
  obtain ⟨b, h, _⟩ := inf_le (α := WithTop α) h _ rfl
  exact ⟨b, h⟩

Existence of Minimum for Nonempty Finite Sets in Linear Orders

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any element $a \in s$, there exists an element $b \in \alpha$ such that the minimum of $s$ (considered in $\text{WithTop}\ \alpha$) is equal to $b$.

Finset.min_of_nonempty theorem

{s : Finset α} (h : s.Nonempty) : ∃ a : α, s.min = a

Full source

theorem min_of_nonempty {s : Finset α} (h : s.Nonempty) : ∃ a : α, s.min = a :=
  let ⟨_, h⟩ := h
  min_of_mem h

Existence of Minimum for Nonempty Finite Sets in Linear Orders

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, there exists an element $a \in \alpha$ such that the minimum of $s$ (considered in $\text{WithTop}\ \alpha$) is equal to $a$.

Finset.min_eq_top theorem

{s : Finset α} : s.min = ⊤ ↔ s = ∅

Full source

@[simp]
theorem min_eq_top {s : Finset α} : s.min = ⊤ ↔ s = ∅ := by
  simp [Finset.min, eq_empty_iff_forall_not_mem]

Minimum Equals Top if and only if Set is Empty

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the minimum of $s$ (considered as an element of $\alpha$ extended with a top element $\top$) equals $\top$ if and only if $s$ is the empty set. In other words, $\min s = \top \leftrightarrow s = \emptyset$.

Finset.mem_of_min theorem

{s : Finset α} : ∀ {a : α}, s.min = a → a ∈ s

Full source

theorem mem_of_min {s : Finset α} : ∀ {a : α}, s.min = a → a ∈ s :=
  @mem_of_max αᵒᵈ _ s

Minimum Element Belongs to Finite Set: $\min(s) = a \implies a \in s$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any element $a \in \alpha$, if the minimum element of $s$ is equal to $a$, then $a$ belongs to $s$.

Finset.min_le theorem

{a : α} {s : Finset α} (as : a ∈ s) : s.min ≤ a

Full source

theorem min_le {a : α} {s : Finset α} (as : a ∈ s) : s.min ≤ a :=
  inf_le as

Minimum Element is a Lower Bound for Finite Sets

Informal description

For any element $a$ in a finite set $s$ of a linearly ordered type $\alpha$, the minimum element of $s$ is less than or equal to $a$, i.e., $\min(s) \leq a$.

Finset.not_mem_of_coe_lt_min theorem

{a : α} {s : Finset α} (h : ↑a < s.min) : a ∉ s

Full source

theorem not_mem_of_coe_lt_min {a : α} {s : Finset α} (h : ↑a < s.min) : a ∉ s :=
  mt min_le h.not_le

Non-membership Criterion via Minimum: $a < \min(s) \implies a \notin s$

Informal description

For any element $a$ in a linearly ordered type $\alpha$ and any finite set $s$ of $\alpha$, if the canonical injection of $a$ into $\text{WithTop}\ \alpha$ is strictly less than the minimum element of $s$, then $a$ does not belong to $s$.

Finset.min_le_of_eq theorem

{s : Finset α} {a b : α} (h₁ : b ∈ s) (h₂ : s.min = a) : a ≤ b

Full source

theorem min_le_of_eq {s : Finset α} {a b : α} (h₁ : b ∈ s) (h₂ : s.min = a) : a ≤ b :=
  WithTop.coe_le_coe.mp <| h₂.ge.trans (min_le h₁)

Minimum Element is a Lower Bound for Finite Sets via Equality

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, if $b$ is an element of $s$ and the minimum of $s$ is equal to $a$, then $a \leq b$.

Finset.not_mem_of_lt_min theorem

{s : Finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = ↑b) : a ∉ s

Full source

theorem not_mem_of_lt_min {s : Finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = ↑b) : a ∉ s :=
  Finset.not_mem_of_coe_lt_min <| (WithTop.coe_lt_coe.mpr h₁).trans_eq h₂.symm

Non-membership via Minimum Comparison: $a < \min(s) = b \implies a \notin s$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and elements $a, b \in \alpha$, if $a < b$ and the minimum of $s$ is equal to $b$ (when viewed in $\text{WithTop}\ \alpha$), then $a$ does not belong to $s$.

Finset.min_union theorem

{s t : Finset α} : (s ∪ t).min = s.min ⊓ t.min

Full source

theorem min_union {s t : Finset α} : (s ∪ t).min = s.min ⊓ t.min := inf_union

Minimum of Union Equals Meet of Minima for Finite Sets

Informal description

For any two finite sets $s$ and $t$ in a linearly ordered type $\alpha$, the minimum of their union $s \cup t$ is equal to the meet (infimum) of their individual minima, i.e., \[ \min(s \cup t) = \min(s) \sqcap \min(t). \] Here, the minima are taken in $\text{WithTop}\ \alpha$, where $\min(\emptyset) = \top$.

Finset.min_mono theorem

{s t : Finset α} (st : s ⊆ t) : t.min ≤ s.min

Full source

@[gcongr]
theorem min_mono {s t : Finset α} (st : s ⊆ t) : t.min ≤ s.min :=
  inf_mono st

Monotonicity of Minimum under Finite Set Inclusion: $s \subseteq t \implies \min t \leq \min s$

Informal description

For any two finite sets $s$ and $t$ in a linearly ordered type $\alpha$, if $s \subseteq t$, then the minimum of $t$ is less than or equal to the minimum of $s$ (where minima are taken in $\text{WithTop}\ \alpha$ and $\min(\emptyset) = \top$).

Finset.le_min theorem

{m : WithTop α} {s : Finset α} (st : ∀ a : α, a ∈ s → m ≤ a) : m ≤ s.min

Full source

protected theorem le_min {m : WithTop α} {s : Finset α} (st : ∀ a : α, a ∈ s → m ≤ a) : m ≤ s.min :=
  Finset.le_inf st

Lower Bound Implies Less Than or Equal to Minimum in Finite Sets

Informal description

Let $\alpha$ be a linearly ordered type with a top element $\top$ in $\text{WithTop}\ \alpha$. For any finite set $s \subseteq \alpha$ and any element $m \in \text{WithTop}\ \alpha$, if $m \leq a$ for all $a \in s$, then $m \leq \min s$.

Finset.le_min_iff theorem

{m : WithTop α} {s : Finset α} : m ≤ s.min ↔ ∀ a ∈ s, m ≤ a

Full source

@[simp]
protected theorem le_min_iff {m : WithTop α} {s : Finset α} : m ≤ s.min ↔ ∀ a ∈ s, m ≤ a :=
  Finset.le_inf_iff

Characterization of Lower Bounds of Finite Set Minimum: $m \leq \min s \leftrightarrow \forall a \in s, m \leq a$

Informal description

For any element $m$ in $\text{WithTop}\ \alpha$ and any finite set $s$ in a linearly ordered type $\alpha$, we have $m \leq \min s$ if and only if $m \leq a$ for every $a \in s$.

Finset.min_eq_bot theorem

[OrderBot α] {s : Finset α} : s.min = ⊥ ↔ ⊥ ∈ s

Full source

@[simp]
protected theorem min_eq_bot [OrderBot α] {s : Finset α} : s.min = ⊥ ↔ ⊥ ∈ s :=
  Finset.max_eq_top (α := αᵒᵈ)

Minimum of Finite Set Equals Bottom Element if and only if Bottom is in Set

Informal description

For a finite set $s$ in a linearly ordered type $\alpha$ with a bottom element $\bot$, the minimum element of $s$ equals $\bot$ if and only if $\bot$ is an element of $s$.

Finset.min' definition

(s : Finset α) (H : s.Nonempty) : α

Full source

/-- 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 min' (s : Finset α) (H : s.Nonempty) : α :=
  inf' s H id

Minimum element of a nonempty finite set in a linear order

Informal description

Given a nonempty finite set $s$ in a linear order $\alpha$, the term $s.\text{min}' H$ is the minimum element of $s$, where $H$ is a proof that $s$ is nonempty. This is defined as the infimum of the identity function over $s$.

Finset.max' definition

(s : Finset α) (H : s.Nonempty) : α

Full source

/-- 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 α`. -/
def max' (s : Finset α) (H : s.Nonempty) : α :=
  sup' s H id

Maximum element of a nonempty finite set in a linear order

Informal description

Given a nonempty finite set $s$ in a linear order $\alpha$, the term $s.\text{max}' H$ is the maximum element of $s$, where $H$ is a proof that $s$ is nonempty. This is defined as the supremum of the identity function over $s$ (using `sup'`).

Finset.min'_mem theorem

: s.min' H ∈ s

Full source

theorem min'_mem : s.min' H ∈ s :=
  mem_of_min <| by simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]

Minimum Element Belongs to Its Set

Informal description

For any nonempty finite set $s$ in a linear order $\alpha$, the minimum element $\min' s H$ belongs to $s$.

Finset.min'_le theorem

(x) (H2 : x ∈ s) : s.min' ⟨x, H2⟩ ≤ x

Full source

theorem min'_le (x) (H2 : x ∈ s) : s.min' ⟨x, H2⟩ ≤ x :=
  min_le_of_eq H2 (WithTop.coe_untop _ _).symm

Minimum Element is a Lower Bound in Finite Sets

Informal description

For any element $x$ in a nonempty finite set $s$ of a linearly ordered type $\alpha$, the minimum element of $s$ (denoted $\min' s H$ where $H$ is a proof that $s$ is nonempty) is less than or equal to $x$.

Finset.le_min' theorem

(x) (H2 : ∀ y ∈ s, x ≤ y) : x ≤ s.min' H

Full source

theorem le_min' (x) (H2 : ∀ y ∈ s, x ≤ y) : x ≤ s.min' H :=
  H2 _ <| min'_mem _ _

Lower Bound is Less Than or Equal to Minimum of Finite Set

Informal description

For any element $x$ in a linear order $\alpha$ and any nonempty finite set $s \subseteq \alpha$, if $x$ is a lower bound for $s$ (i.e., $x \leq y$ for all $y \in s$), then $x$ is less than or equal to the minimum element of $s$, denoted $\min' s H$, where $H$ is a proof that $s$ is nonempty.

Finset.isLeast_min' theorem

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

Full source

theorem isLeast_min' : IsLeast (↑s) (s.min' H) :=
  ⟨min'_mem _ _, min'_le _⟩

Minimum Element is the Least Element in a Finite Set

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the minimum element $\min' s H$ is the least element of $s$, i.e., it belongs to $s$ and is less than or equal to every element of $s$.

Finset.le_min'_iff theorem

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

Full source

@[simp]
theorem le_min'_iff {x} : x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y :=
  le_isGLB_iff (isLeast_min' s H).isGLB

Characterization of Minimum Element in Finite Sets: $x \leq \min' s H \leftrightarrow \forall y \in s, x \leq y$

Informal description

For any element $x$ in a linear order $\alpha$ and any nonempty finite set $s \subseteq \alpha$, the inequality $x \leq \min' s H$ holds if and only if $x$ is a lower bound for $s$, i.e., $x \leq y$ for all $y \in s$.

Finset.min'_singleton theorem

(a : α) : ({ a } : Finset α).min' (singleton_nonempty _) = a

Full source

/-- `{a}.min' _` is `a`. -/
@[simp]
theorem min'_singleton (a : α) : ({a} : Finset α).min' (singleton_nonempty _) = a := by simp [min']

Minimum of Singleton Set is Its Element

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the minimum of the singleton set $\{a\}$ is $a$ itself, i.e., $\min'(\{a\}) = a$.

Finset.max'_mem theorem

: s.max' H ∈ s

Full source

theorem max'_mem : s.max' H ∈ s :=
  mem_of_max <| by simp only [max', Finset.max, id_eq, coe_sup', Function.comp_def]

Maximum Element Belongs to Finite Set: $\max'(s) \in s$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the maximum element $\max' s H$ belongs to $s$.

Finset.le_max' theorem

(x) (H2 : x ∈ s) : x ≤ s.max' ⟨x, H2⟩

Full source

theorem le_max' (x) (H2 : x ∈ s) : x ≤ s.max' ⟨x, H2⟩ :=
  le_max_of_eq H2 (WithBot.coe_unbot _ _).symm

Element in Finite Set is Bounded by its Maximum: $x \leq \max'(s)$ for $x \in s$

Informal description

For any element $x$ in a finite set $s$ of a linearly ordered type $\alpha$, we have $x \leq \max'(s)$, where $\max'(s)$ is the maximum element of $s$ (which exists since $s$ is nonempty by virtue of containing $x$).

Finset.max'_le theorem

(x) (H2 : ∀ y ∈ s, y ≤ x) : s.max' H ≤ x

Full source

theorem max'_le (x) (H2 : ∀ y ∈ s, y ≤ x) : s.max' H ≤ x :=
  H2 _ <| max'_mem _ _

Maximum Element is Least Upper Bound for Finite Set

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, if every element $y \in s$ satisfies $y \leq x$ for some $x \in \alpha$, then the maximum element $\max'(s, H)$ of $s$ (where $H$ is a proof that $s$ is nonempty) also satisfies $\max'(s, H) \leq x$.

Finset.isGreatest_max' theorem

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

Full source

theorem isGreatest_max' : IsGreatest (↑s) (s.max' H) :=
  ⟨max'_mem _ _, le_max' _⟩

Maximum Element is Greatest in Finite Set

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the maximum element $\max'(s, H)$ is the greatest element of $s$, meaning $\max'(s, H) \in s$ and for all $y \in s$, $y \leq \max'(s, H)$.

Finset.max'_le_iff theorem

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

Full source

@[simp]
theorem max'_le_iff {x} : s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x :=
  isLUB_le_iff (isGreatest_max' s H).isLUB

Characterization of Maximum Element: $\max'(s) \leq x \leftrightarrow \forall y \in s, y \leq x$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$ and any element $x \in \alpha$, the maximum element $\max'(s, H)$ of $s$ is less than or equal to $x$ if and only if every element $y \in s$ satisfies $y \leq x$.

Finset.max'_lt_iff theorem

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

Full source

@[simp]
theorem max'_lt_iff {x} : s.max' H < x ↔ ∀ y ∈ s, y < x :=
  ⟨fun Hlt y hy => (s.le_max' y hy).trans_lt Hlt, fun H => H _ <| s.max'_mem _⟩

Characterization of Maximum Element Strictly Less Than a Given Value: $\max'(s) < x \leftrightarrow \forall y \in s, y < x$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$ and any element $x \in \alpha$, the maximum element $\max'(s)$ of $s$ is strictly less than $x$ if and only if every element $y \in s$ is strictly less than $x$.

Finset.lt_min'_iff theorem

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

Full source

@[simp]
theorem lt_min'_iff : x < s.min' H ↔ ∀ y ∈ s, x < y :=
  @max'_lt_iff αᵒᵈ _ _ H _

Characterization of Elements Strictly Less Than the Minimum: $x < \min'(s) \leftrightarrow \forall y \in s, x < y$

Informal description

For any element $x$ in a linearly ordered type $\alpha$ and any nonempty finite set $s$ in $\alpha$, the element $x$ is strictly less than the minimum element $\min'(s)$ of $s$ if and only if $x$ is strictly less than every element $y$ in $s$.

Finset.max'_eq_sup' theorem

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

Full source

theorem max'_eq_sup' : s.max' H = s.sup' H id := rfl

Maximum Equals Supremum of Identity Function on Finite Set

Informal description

For any nonempty finite set $s$ in a linear order $\alpha$, the maximum element $s.\text{max}' H$ is equal to the supremum of the identity function over $s$, i.e., $\max s = \sup_{x \in s} x$.

Finset.min'_eq_inf' theorem

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

Full source

theorem min'_eq_inf' : s.min' H = s.inf' H id := rfl

Minimum Equals Infimum of Identity Function on Finite Set

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the minimum element $\min' s$ is equal to the infimum of the identity function over $s$, i.e., $\min' s = \inf_{x \in s} x$.

Finset.max'_singleton theorem

(a : α) : ({ a } : Finset α).max' (singleton_nonempty _) = a

Full source

/-- `{a}.max' _` is `a`. -/
@[simp]
theorem max'_singleton (a : α) : ({a} : Finset α).max' (singleton_nonempty _) = a := by simp [max']

Maximum of Singleton Set is Its Element

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the maximum element of the singleton set $\{a\}$ is $a$ itself, i.e., $\max'(\{a\}) = a$.

Finset.min'_lt_max' theorem

{i j} (H1 : i ∈ s) (H2 : j ∈ s) (H3 : i ≠ j) : s.min' ⟨i, H1⟩ < s.max' ⟨i, H1⟩

Full source

theorem min'_lt_max' {i j} (H1 : i ∈ s) (H2 : j ∈ s) (H3 : i ≠ j) :
    s.min' ⟨i, H1⟩ < s.max' ⟨i, H1⟩ :=
  isGLB_lt_isLUB_of_ne (s.isLeast_min' _).isGLB (s.isGreatest_max' _).isLUB H1 H2 H3

Minimum is Less Than Maximum in Finite Sets with Distinct Elements

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, if $i$ and $j$ are distinct elements of $s$, then the minimum element of $s$ (with witness $i$) is strictly less than the maximum element of $s$ (with witness $i$). In other words, if $s$ contains at least two distinct elements, then $\min(s) < \max(s)$.

Finset.min'_lt_max'_of_card theorem

(h₂ : 1 < card s) : s.min' (Finset.card_pos.1 <| by omega) < s.max' (Finset.card_pos.1 <| by omega)

Full source

/-- 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 min'_lt_max'_of_card (h₂ : 1 < card s) :
    s.min' (Finset.card_pos.1 <| by omega) < s.max' (Finset.card_pos.1 <| by omega) := by
  rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
  exact s.min'_lt_max' ha hb hab

Minimum is Less Than Maximum in Finite Sets of Cardinality Greater Than One

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, if the cardinality of $s$ is greater than 1, then the minimum element of $s$ is strictly less than the maximum element of $s$, i.e., \[ \min(s) < \max(s). \]

Finset.max'_union theorem

 {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
  (s₁ ∪ s₂).max' (h₁.mono subset_union_left) = s₁.max' h₁ ⊔ s₂.max' h₂

Full source

theorem max'_union {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
    (s₁ ∪ s₂).max' (h₁.mono subset_union_left) = s₁.max' h₁ ⊔ s₂.max' h₂ := sup'_union h₁ h₂ id

Maximum of Union of Nonempty Finite Sets

Informal description

For any nonempty finite sets $s₁$ and $s₂$ in a linearly ordered type $\alpha$, the maximum element of their union $s₁ \cup s₂$ is equal to the maximum of the maximum elements of $s₁$ and $s₂$, i.e., \[ \max(s₁ \cup s₂) = \max(\max s₁, \max s₂). \]

Finset.min'_union theorem

 {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
  (s₁ ∪ s₂).min' (h₁.mono subset_union_left) = s₁.min' h₁ ⊓ s₂.min' h₂

Full source

theorem min'_union {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) :
    (s₁ ∪ s₂).min' (h₁.mono subset_union_left) = s₁.min' h₁ ⊓ s₂.min' h₂ := inf'_union h₁ h₂ id

Minimum of Union of Nonempty Finite Sets in a Linear Order

Informal description

For any nonempty finite sets $s_1$ and $s_2$ in a linearly ordered type $\alpha$, the minimum element of their union $s_1 \cup s_2$ is equal to the minimum of the minimum elements of $s_1$ and $s_2$, i.e., \[ \min(s_1 \cup s_2) = \min(\min s_1, \min s_2). \]

Finset.map_ofDual_min theorem

(s : Finset αᵒᵈ) : s.min.map ofDual = (s.image ofDual).max

Full source

theorem map_ofDual_min (s : Finset αᵒᵈ) : s.min.map ofDual = (s.image ofDual).max := by
  rw [max_eq_sup_withBot, sup_image]
  exact congr_fun Option.map_id _

Minimum in Order Dual Maps to Maximum under Dual Isomorphism

Informal description

Let $s$ be a finite set in the order dual $\alpha^{\text{op}}$ of a linearly ordered type $\alpha$. Then the minimum of $s$ (considered in $\text{WithTop}\ \alpha^{\text{op}}$) mapped under the order dual isomorphism $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ equals the maximum of the image of $s$ under $\text{ofDual}$ in $\alpha$.

Finset.map_ofDual_max theorem

(s : Finset αᵒᵈ) : s.max.map ofDual = (s.image ofDual).min

Full source

theorem map_ofDual_max (s : Finset αᵒᵈ) : s.max.map ofDual = (s.image ofDual).min := by
  rw [min_eq_inf_withTop, inf_image]
  exact congr_fun Option.map_id _

Maximum in Order Dual Maps to Minimum under Dual Isomorphism

Informal description

Let $s$ be a finite set in the order dual $\alpha^{\text{op}}$ of a linearly ordered type $\alpha$. Then the maximum of $s$ (considered in $\text{WithBot}\ \alpha^{\text{op}}$) mapped under the order dual isomorphism $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ equals the minimum of the image of $s$ under $\text{ofDual}$ in $\alpha$. In symbols: \[ \text{ofDual}(\max s) = \min (\text{ofDual}(s)). \]

Finset.map_toDual_min theorem

(s : Finset α) : s.min.map toDual = (s.image toDual).max

Full source

theorem map_toDual_min (s : Finset α) : s.min.map toDual = (s.image toDual).max := by
  rw [max_eq_sup_withBot, sup_image]
  exact congr_fun Option.map_id _

Minimum in Original Order Equals Maximum in Dual Order via $\text{toDual}$

Informal description

For any finite set $s$ of elements in a linearly ordered type $\alpha$, the minimum of $s$ (considered in $\text{WithTop}\ \alpha$) mapped to the order dual $\alpha^{\text{op}}$ via the canonical equivalence $\text{toDual} : \alpha \to \alpha^{\text{op}}$ is equal to the maximum of the image of $s$ under $\text{toDual}$ (considered in $\text{WithBot}\ \alpha^{\text{op}}$). In other words, if we denote the minimum operation on $s$ as $\min s$ (which returns $\top$ if $s$ is empty) and the maximum operation on the image of $s$ under $\text{toDual}$ as $\max (\text{toDual}(s))$ (which returns $\bot$ if $s$ is empty), then: \[ \text{toDual}(\min s) = \max (\text{toDual}(s)). \]

Finset.map_toDual_max theorem

(s : Finset α) : s.max.map toDual = (s.image toDual).min

Full source

theorem map_toDual_max (s : Finset α) : s.max.map toDual = (s.image toDual).min := by
  rw [min_eq_inf_withTop, inf_image]
  exact congr_fun Option.map_id _

Maximum in Original Order Equals Minimum in Dual Order via $\text{toDual}$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the maximum element of $s$ (considered in $\text{WithBot}\ \alpha$) mapped to the order dual $\alpha^{\text{op}}$ via the canonical equivalence $\text{toDual} : \alpha \to \alpha^{\text{op}}$ is equal to the minimum of the image of $s$ under $\text{toDual}$ (considered in $\text{WithTop}\ \alpha^{\text{op}}$). In other words, if we denote the maximum operation on $s$ as $\max s$ (which returns $\bot$ if $s$ is empty) and the minimum operation on the image of $s$ under $\text{toDual}$ as $\min (\text{toDual}(s))$ (which returns $\top$ if $s$ is empty), then: \[ \text{toDual}(\max s) = \min (\text{toDual}(s)). \]

Finset.ofDual_min' theorem

{s : Finset αᵒᵈ} (hs : s.Nonempty) : ofDual (min' s hs) = max' (s.image ofDual) (hs.image _)

Full source

theorem ofDual_min' {s : Finset αᵒᵈ} (hs : s.Nonempty) :
    ofDual (min' s hs) = max' (s.image ofDual) (hs.image _) := by
  rw [← WithBot.coe_eq_coe]
  simp [min'_eq_inf', max'_eq_sup']

Minimum in Dual Order Equals Maximum in Original Order via $\text{ofDual}$

Informal description

For any nonempty finite set $s$ in the order dual $\alpha^{\text{op}}$ of a linearly ordered type $\alpha$, the minimum element of $s$ in $\alpha^{\text{op}}$ (when mapped back to $\alpha$ via the canonical equivalence $\text{ofDual} : \alpha^{\text{op}} \to \alpha$) is equal to the maximum element of the image of $s$ under $\text{ofDual}$ in $\alpha$. In other words, if $s$ is a nonempty finite subset of $\alpha^{\text{op}}$, then: \[ \text{ofDual}(\min' s H) = \max' (\text{ofDual}(s)) H', \] where $H$ is a proof that $s$ is nonempty and $H'$ is the corresponding proof that $\text{ofDual}(s)$ is nonempty.

Finset.ofDual_max' theorem

{s : Finset αᵒᵈ} (hs : s.Nonempty) : ofDual (max' s hs) = min' (s.image ofDual) (hs.image _)

Full source

theorem ofDual_max' {s : Finset αᵒᵈ} (hs : s.Nonempty) :
    ofDual (max' s hs) = min' (s.image ofDual) (hs.image _) := by
  rw [← WithTop.coe_eq_coe]
  simp [min'_eq_inf', max'_eq_sup']

Duality of Maximum in Order Dual and Minimum in Original Order

Informal description

For any nonempty finite set $s$ in the order dual $\alpha^{\text{op}}$ of a linearly ordered type $\alpha$, the image under the duality map $\text{ofDual}$ of the maximum element of $s$ in $\alpha^{\text{op}}$ is equal to the minimum element of the image of $s$ under $\text{ofDual}$ in $\alpha$. That is, \[ \text{ofDual}(\max' s H) = \min' (\text{ofDual}(s)) H', \] where $H$ is a proof that $s$ is nonempty and $H'$ is the corresponding proof that $\text{ofDual}(s)$ is nonempty.

Finset.toDual_min' theorem

{s : Finset α} (hs : s.Nonempty) : toDual (min' s hs) = max' (s.image toDual) (hs.image _)

Full source

theorem toDual_min' {s : Finset α} (hs : s.Nonempty) :
    toDual (min' s hs) = max' (s.image toDual) (hs.image _) := by
  rw [← WithBot.coe_eq_coe]
  simp [min'_eq_inf', max'_eq_sup']

Duality of Minimum and Maximum in Finite Sets

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the dual of the minimum element of $s$ is equal to the maximum element of the image of $s$ under the order duality map. That is, if $m = \min s$, then $\text{toDual}(m) = \max (\text{toDual} \circ s)$.

Finset.toDual_max' theorem

{s : Finset α} (hs : s.Nonempty) : toDual (max' s hs) = min' (s.image toDual) (hs.image _)

Full source

theorem toDual_max' {s : Finset α} (hs : s.Nonempty) :
    toDual (max' s hs) = min' (s.image toDual) (hs.image _) := by
  rw [← WithTop.coe_eq_coe]
  simp [min'_eq_inf', max'_eq_sup']

Duality of Maximum and Minimum in Finite Sets

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the order dual of the maximum element of $s$ is equal to the minimum element of the image of $s$ under the order duality map. That is, if $M = \max s$, then $\text{toDual}(M) = \min (\text{toDual} \circ s)$.

Finset.max'_subset theorem

{s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) : s.max' H ≤ t.max' (H.mono hst)

Full source

theorem max'_subset {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) :
    s.max' H ≤ t.max' (H.mono hst) :=
  le_max' _ _ (hst (s.max'_mem H))

Monotonicity of Maximum under Subset Inclusion: $\max(s) \leq \max(t)$ for $s \subseteq t$

Informal description

For any nonempty finite subsets $s$ and $t$ of a linearly ordered type $\alpha$, if $s \subseteq t$, then the maximum element of $s$ is less than or equal to the maximum element of $t$.

Finset.min'_subset theorem

{s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) : t.min' (H.mono hst) ≤ s.min' H

Full source

theorem min'_subset {s t : Finset α} (H : s.Nonempty) (hst : s ⊆ t) :
    t.min' (H.mono hst) ≤ s.min' H :=
  min'_le _ _ (hst (s.min'_mem H))

Monotonicity of Minimum under Subset Inclusion: $\min(t) \leq \min(s)$ for $s \subseteq t$

Informal description

For any nonempty finite subsets $s$ and $t$ of a linearly ordered type $\alpha$, if $s \subseteq t$, then the minimum element of $t$ is less than or equal to the minimum element of $s$.

Finset.max'_insert theorem

(a : α) (s : Finset α) (H : s.Nonempty) : (insert a s).max' (s.insert_nonempty a) = max (s.max' H) a

Full source

theorem max'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
    (insert a s).max' (s.insert_nonempty a) = max (s.max' H) a :=
  (isGreatest_max' _ _).unique <| by
    rw [coe_insert, max_comm]
    exact (isGreatest_max' _ _).insert _

Maximum of Inserted Element and Finite Set: $\max'(\{a\} \cup s) = \max(\max'(s), a)$

Informal description

For any element $a$ in a linearly ordered type $\alpha$ and any nonempty finite subset $s$ of $\alpha$, the maximum element of the set $\{a\} \cup s$ is equal to the maximum of $a$ and the maximum element of $s$, i.e., $$\max'(\{a\} \cup s) = \max(\max'(s), a).$$

Finset.min'_insert theorem

(a : α) (s : Finset α) (H : s.Nonempty) : (insert a s).min' (s.insert_nonempty a) = min (s.min' H) a

Full source

theorem min'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
    (insert a s).min' (s.insert_nonempty a) = min (s.min' H) a :=
  (isLeast_min' _ _).unique <| by
    rw [coe_insert, min_comm]
    exact (isLeast_min' _ _).insert _

Minimum of Inserted Element and Finite Set: $\min'(\{a\} \cup s) = \min(\min'(s), a)$

Informal description

For any element $a$ in a linearly ordered type $\alpha$ and any nonempty finite subset $s$ of $\alpha$, the minimum element of the set $\{a\} \cup s$ is equal to the minimum of $a$ and the minimum element of $s$, i.e., $$\min'(\{a\} \cup s) = \min(\min'(s), a).$$

Finset.lt_max'_of_mem_erase_max' theorem

[DecidableEq α] {a : α} (ha : a ∈ s.erase (s.max' H)) : a < s.max' H

Full source

theorem lt_max'_of_mem_erase_max' [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.max' H)) :
    a < s.max' H :=
  lt_of_le_of_ne (le_max' _ _ (mem_of_mem_erase ha)) <| ne_of_mem_of_not_mem ha <| not_mem_erase _ _

Elements Below Maximum in Finite Set: $a \in s \setminus \{\max' s\} \implies a < \max' s$

Informal description

Let $\alpha$ be a linearly ordered type with decidable equality, $s$ a nonempty finite subset of $\alpha$, and $a$ an element of $s$ that is not equal to the maximum element of $s$. Then $a$ is strictly less than the maximum element of $s$, i.e., $a < \max' s$.

Finset.min'_lt_of_mem_erase_min' theorem

[DecidableEq α] {a : α} (ha : a ∈ s.erase (s.min' H)) : s.min' H < a

Full source

theorem min'_lt_of_mem_erase_min' [DecidableEq α] {a : α} (ha : a ∈ s.erase (s.min' H)) :
    s.min' H < a :=
  @lt_max'_of_mem_erase_max' αᵒᵈ _ s H _ a ha

Elements Above Minimum in Finite Set: $\min' s < a$ for $a \in s \setminus \{\min' s\}$

Informal description

Let $\alpha$ be a linearly ordered type with decidable equality, $s$ a nonempty finite subset of $\alpha$, and $a$ an element of $s$ that is not equal to the minimum element of $s$. Then the minimum element of $s$ is strictly less than $a$, i.e., $\min' s < a$.

Finset.max'_image theorem

 [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) (h : (s.image f).Nonempty) :
  (s.image f).max' h = f (s.max' h.of_image)

Full source

/-- To rewrite from right to left, use `Monotone.map_finset_max'`. -/
@[simp]
theorem max'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α)
    (h : (s.image f).Nonempty) : (s.image f).max' h = f (s.max' h.of_image) := by
  simp only [max', sup'_image]
  exact .symm <| comp_sup'_eq_sup'_comp _ _ fun _ _ ↦ hf.map_max

Monotone Function Preserves Maximum: $\max' f(s) = f(\max' s)$

Informal description

Let $\alpha$ and $\beta$ be linearly ordered types, $f : \alpha \to \beta$ a monotone function, and $s$ a nonempty finite subset of $\alpha$. Then the maximum element of the image $f(s)$ is equal to $f$ applied to the maximum element of $s$, i.e., \[ \max' (f(s)) = f(\max' s). \]

Monotone.map_finset_max' theorem

 [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) :
  f (s.max' h) = (s.image f).max' (h.image f)

Full source

/-- A version of `Finset.max'_image` with LHS and RHS reversed.
Also, this version assumes that `s` is nonempty, not its image. -/
lemma _root_.Monotone.map_finset_max' [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α}
    (h : s.Nonempty) : f (s.max' h) = (s.image f).max' (h.image f) :=
  .symm <| max'_image hf ..

Monotone Function Preserves Maximum: $f(\max' s) = \max' f(s)$

Informal description

Let $\alpha$ and $\beta$ be linearly ordered types, $f : \alpha \to \beta$ a monotone function, and $s$ a nonempty finite subset of $\alpha$. Then the image of the maximum element of $s$ under $f$ is equal to the maximum element of the image $f(s)$, i.e., \[ f(\max' s) = \max' (f(s)). \]

Finset.min'_image theorem

 [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) (h : (s.image f).Nonempty) :
  (s.image f).min' h = f (s.min' h.of_image)

Full source

/-- To rewrite from right to left, use `Monotone.map_finset_min'`. -/
@[simp]
theorem min'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α)
    (h : (s.image f).Nonempty) : (s.image f).min' h = f (s.min' h.of_image) := by
  simp only [min', inf'_image]
  exact .symm <| comp_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

Monotone Function Preserves Minimum: $\min' f(s) = f(\min' s)$

Informal description

Let $\alpha$ and $\beta$ be linearly ordered types, $f : \alpha \to \beta$ a monotone function, and $s$ a nonempty finite subset of $\alpha$. Then the minimum element of the image $f(s)$ is equal to $f$ applied to the minimum element of $s$, i.e., \[ \min' (f(s)) = f(\min' s). \]

Monotone.map_finset_min' theorem

 [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) :
  f (s.min' h) = (s.image f).min' (h.image f)

Full source

/-- A version of `Finset.min'_image` with LHS and RHS reversed.
Also, this version assumes that `s` is nonempty, not its image. -/
lemma _root_.Monotone.map_finset_min' [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α}
    (h : s.Nonempty) : f (s.min' h) = (s.image f).min' (h.image f) :=
  .symm <| min'_image hf ..

Monotone Function Preserves Minimum: $f(\min' s) = \min' f(s)$

Informal description

Let $\alpha$ and $\beta$ be linearly ordered types, $f : \alpha \to \beta$ a monotone function, and $s$ a nonempty finite subset of $\alpha$. Then the image of the minimum element of $s$ under $f$ is equal to the minimum element of the image $f(s)$, i.e., \[ f(\min' s) = \min' (f(s)). \]

Finset.coe_max' theorem

{s : Finset α} (hs : s.Nonempty) : ↑(s.max' hs) = s.max

Full source

theorem coe_max' {s : Finset α} (hs : s.Nonempty) : ↑(s.max' hs) = s.max :=
  coe_sup' hs id

Embedding of Maximum Element Commutes with Finite Supremum in $\text{WithBot }\alpha$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the embedding of the maximum element $s.\text{max}'$ (where $\text{max}'$ is the maximum element of $s$) into $\text{WithBot }\alpha$ is equal to the maximum of $s$ in $\text{WithBot }\alpha$. That is, $$(s.\text{max}' : \text{WithBot }\alpha) = s.\text{max}$$ where $s.\text{max}$ is the supremum of $s$ in $\text{WithBot }\alpha$.

Finset.coe_min' theorem

{s : Finset α} (hs : s.Nonempty) : ↑(s.min' hs) = s.min

Full source

theorem coe_min' {s : Finset α} (hs : s.Nonempty) : ↑(s.min' hs) = s.min :=
  coe_inf' hs id

Embedding of Minimum Element Commutes with Finite Infimum in $\text{WithTop }\alpha$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the embedding of the minimum element $s.\min'$ (where $\min'$ is the minimum element of $s$) into $\text{WithTop }\alpha$ is equal to the minimum of $s$ in $\text{WithTop }\alpha$. That is, $$(s.\min' : \text{WithTop }\alpha) = s.\min$$ where $s.\min$ is the infimum of $s$ in $\text{WithTop }\alpha$.

Finset.max_mem_image_coe theorem

{s : Finset α} (hs : s.Nonempty) : s.max ∈ (s.image (↑) : Finset (WithBot α))

Full source

theorem max_mem_image_coe {s : Finset α} (hs : s.Nonempty) :
    s.max ∈ (s.image (↑) : Finset (WithBot α)) :=
  mem_image.2 ⟨max' s hs, max'_mem _ _, coe_max' hs⟩

Maximum of Finite Set Belongs to its Embedding in $\text{WithBot }\alpha$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the maximum element $s.\max$ (viewed in $\text{WithBot }\alpha$) belongs to the image of $s$ under the canonical embedding $\alpha \to \text{WithBot }\alpha$. In other words, if $s$ is nonempty, then $s.\max$ is equal to the embedding of some element of $s$ into $\text{WithBot }\alpha$.

Finset.min_mem_image_coe theorem

{s : Finset α} (hs : s.Nonempty) : s.min ∈ (s.image (↑) : Finset (WithTop α))

Full source

theorem min_mem_image_coe {s : Finset α} (hs : s.Nonempty) :
    s.min ∈ (s.image (↑) : Finset (WithTop α)) :=
  mem_image.2 ⟨min' s hs, min'_mem _ _, coe_min' hs⟩

Minimum of Finite Set Belongs to its Embedding in $\text{WithTop }\alpha$

Informal description

For any nonempty finite set $s$ in a linearly ordered type $\alpha$, the minimum element $\min s$ (viewed in $\text{WithTop }\alpha$) belongs to the image of $s$ under the canonical embedding $\alpha \to \text{WithTop }\alpha$. In other words, if $s$ is nonempty, then $\min s$ is equal to the embedding of some element of $s$ into $\text{WithTop }\alpha$.

Finset.max_mem_insert_bot_image_coe theorem

(s : Finset α) : s.max ∈ (insert ⊥ (s.image (↑)) : Finset (WithBot α))

Full source

theorem max_mem_insert_bot_image_coe (s : Finset α) :
    s.max ∈ (insert ⊥ (s.image (↑)) : Finset (WithBot α)) :=
  mem_insert.2 <| s.eq_empty_or_nonempty.imp max_eq_bot.2 max_mem_image_coe

Maximum of Finite Set Belongs to its Embedding with Bottom Element

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the maximum element of $s$ (viewed in $\text{WithBot }\alpha$) belongs to the set obtained by inserting the bottom element $\bot$ into the image of $s$ under the canonical embedding $\alpha \to \text{WithBot }\alpha$. In other words, $s.\max$ is either $\bot$ (if $s$ is empty) or the embedding of some element of $s$ into $\text{WithBot }\alpha$.

Finset.min_mem_insert_top_image_coe theorem

(s : Finset α) : s.min ∈ (insert ⊤ (s.image (↑)) : Finset (WithTop α))

Full source

theorem min_mem_insert_top_image_coe (s : Finset α) :
    s.min ∈ (insert ⊤ (s.image (↑)) : Finset (WithTop α)) :=
  mem_insert.2 <| s.eq_empty_or_nonempty.imp min_eq_top.2 min_mem_image_coe

Minimum of Finite Set Belongs to Extended Set with Top Element

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$, the minimum element $\min s$ (considered in $\text{WithTop}\ \alpha$) belongs to the set obtained by inserting the top element $\top$ into the image of $s$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$. In other words, $\min s \in \{\top\} \cup \{a \mid a \in s\}$.

Finset.max'_erase_ne_self theorem

{s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).max' s0 ≠ x

Full source

theorem max'_erase_ne_self {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).max' s0 ≠ x :=
  ne_of_mem_erase (max'_mem _ s0)

Maximum of Finite Set Minus Element is Not That Element

Informal description

For any finite set $s$ of elements in a linearly ordered type $\alpha$, and for any element $x \in \alpha$, if the set $s \setminus \{x\}$ is nonempty, then the maximum element of $s \setminus \{x\}$ is not equal to $x$.

Finset.min'_erase_ne_self theorem

{s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).min' s0 ≠ x

Full source

theorem min'_erase_ne_self {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.erase x).min' s0 ≠ x :=
  ne_of_mem_erase (min'_mem _ s0)

Minimum of Finite Set Minus Element is Not That Element

Informal description

For any finite set $s$ of elements in a linearly ordered type $\alpha$, and for any element $x \in \alpha$, if the set $s \setminus \{x\}$ is nonempty, then the minimum element of $s \setminus \{x\}$ is not equal to $x$.

Finset.max_erase_ne_self theorem

{s : Finset α} : (s.erase x).max ≠ x

Full source

theorem max_erase_ne_self {s : Finset α} : (s.erase x).max ≠ x := by
  by_cases s0 : (s.erase x).Nonempty
  · refine ne_of_eq_of_ne (coe_max' s0).symm ?_
    exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
  · rw [not_nonempty_iff_eq_empty.mp s0, max_empty]
    exact WithBot.bot_ne_coe

Maximum of Finite Set Minus Element is Not That Element in $\text{WithBot}\,\alpha$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any element $x \in \alpha$, the maximum element of the set $s \setminus \{x\}$ (viewed in $\text{WithBot}\,\alpha$) is not equal to $x$.

Finset.min_erase_ne_self theorem

{s : Finset α} : (s.erase x).min ≠ x

Full source

theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x := by
  apply mt (congr_arg (WithTop.map toDual))
  rw [map_toDual_min, image_erase toDual.injective, WithTop.map_coe]
  apply max_erase_ne_self

Minimum of Finite Set Minus Element is Not That Element in $\text{WithTop}\,\alpha$

Informal description

For any finite set $s$ in a linearly ordered type $\alpha$ and any element $x \in \alpha$, the minimum element of the set $s \setminus \{x\}$ (viewed in $\text{WithTop}\,\alpha$) is not equal to $x$.

Finset.exists_next_right theorem

{x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) : ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z

Full source

theorem exists_next_right {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) :
    ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z :=
  have Hne : (s.filter (x < ·)).Nonempty := h.imp fun y hy => mem_filter.2 (by simpa)
  have aux := mem_filter.1 (min'_mem _ Hne)
  ⟨min' _ Hne, aux.1, by simp, fun z hzs hz => min'_le _ _ <| mem_filter.2 ⟨hzs, by simpa⟩⟩

Existence of Minimal Right Successor in Finite Sets

Informal description

For any element $x$ in a linearly ordered type $\alpha$ and any finite set $s \subseteq \alpha$, if there exists an element $y \in s$ such that $x < y$, then there exists a minimal such element $y \in s$ satisfying $x < y$ and for all $z \in s$ with $x < z$, we have $y \leq z$.

Finset.exists_next_left theorem

{x : α} {s : Finset α} (h : ∃ y ∈ s, y < x) : ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y

Full source

theorem exists_next_left {x : α} {s : Finset α} (h : ∃ y ∈ s, y < x) :
    ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y :=
  @exists_next_right αᵒᵈ _ x s h

Existence of Maximal Left Predecessor in Finite Sets

Informal description

For any element $x$ in a linearly ordered type $\alpha$ and any finite set $s \subseteq \alpha$, if there exists an element $y \in s$ such that $y < x$, then there exists a maximal such element $y \in s$ satisfying $y < x$ and for all $z \in s$ with $z < x$, we have $z \leq y$.

Finset.card_le_of_interleaved theorem

 {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

Full source

/-- If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card t + 1`. -/
theorem card_le_of_interleaved {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 := by
  replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
    intro x hx y hy hxy
    rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
    rcases h x hx a has hxa fun z hzs hz => hz.2.not_le <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
    exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
  set f : α → WithTop α := fun x => (t.filter fun y => x < y).min
  have f_mono : StrictMonoOn f s := by
    intro x hx y hy hxy
    rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
    calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)

  calc
    s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
    _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
      card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)
    _ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

Cardinality Bound for Interleaved Finite Sets: $|s| \leq |t| + 1$

Informal description

For any two finite sets $s$ and $t$ in a linearly ordered type $\alpha$, if for any two elements $x, y \in s$ with $x < y$ such that there are no elements of $s$ strictly between $x$ and $y$, there exists an element $z \in t$ with $x < z < y$, then the cardinality of $s$ is at most the cardinality of $t$ plus one, i.e., $|s| \leq |t| + 1$.

Finset.card_le_diff_of_interleaved theorem

 {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

Full source

/-- If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card (t \ s) + 1`. -/
theorem card_le_diff_of_interleaved {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 :=
  card_le_of_interleaved fun x hx y hy hxy hs =>
    let ⟨z, hzt, hxz, hzy⟩ := h x hx y hy hxy hs
    ⟨z, mem_sdiff.2 ⟨hzt, fun hzs => hs z hzs ⟨hxz, hzy⟩⟩, hxz, hzy⟩

Cardinality Bound for Interleaved Finite Sets: $|s| \leq |t \setminus s| + 1$

Informal description

For any two finite sets $s$ and $t$ in a linearly ordered type $\alpha$, if for any two elements $x, y \in s$ with $x < y$ such that there are no elements of $s$ strictly between $x$ and $y$, there exists an element $z \in t$ with $x < z < y$, then the cardinality of $s$ is at most the cardinality of $t \setminus s$ plus one, i.e., $|s| \leq |t \setminus s| + 1$.

Finset.induction_on_max theorem

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

Full source

/-- Induction principle for `Finset`s 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)`. -/
@[elab_as_elim]
theorem induction_on_max [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅)
    (step : ∀ a s, (∀ x ∈ s, x < a) → p s → p (insert a s)) : p s := by
  induction' s using Finset.strongInductionOn with s ihs
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · exact h0
  · have H : s.max' hne ∈ s := max'_mem s hne
    rw [← insert_erase H]
    exact step _ _ (fun x => s.lt_max'_of_mem_erase_max' hne) (ihs _ <| erase_ssubset H)

Induction Principle for Finite Sets via Maximum Elements

Informal description

Let $\alpha$ be a linearly ordered type with decidable equality, and let $p$ be a predicate on finite subsets of $\alpha$. To prove that $p(s)$ holds for any finite set $s \subseteq \alpha$, it suffices to show: 1. $p(\emptyset)$ holds for the empty set, 2. For any element $a \in \alpha$ and any finite set $s \subseteq \alpha$, if $a$ is strictly greater than all elements of $s$ (i.e., $x < a$ for all $x \in s$) and $p(s)$ holds, then $p(s \cup \{a\})$ also holds.

Finset.induction_on_min theorem

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

Full source

/-- Induction principle for `Finset`s 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)`. -/
@[elab_as_elim]
theorem induction_on_min [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅)
    (step : ∀ a s, (∀ x ∈ s, a < x) → p s → p (insert a s)) : p s :=
  @induction_on_max αᵒᵈ _ _ _ s h0 step

Induction Principle for Finite Sets via Minimum Elements

Informal description

Let $\alpha$ be a linearly ordered type with decidable equality, and let $p$ be a predicate on finite subsets of $\alpha$. To prove that $p(s)$ holds for any finite set $s \subseteq \alpha$, it suffices to show: 1. $p(\emptyset)$ holds for the empty set, 2. For any element $a \in \alpha$ and any finite set $s \subseteq \alpha$, if $a$ is strictly less than all elements of $s$ (i.e., $a < x$ for all $x \in s$) and $p(s)$ holds, then $p(s \cup \{a\})$ also holds.

Finset.induction_on_max_value theorem

 [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅)
  (step : ∀ a s, a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)) : p s

Full source

/-- Induction principle for `Finset`s 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)`. -/
@[elab_as_elim]
theorem induction_on_max_value [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι)
    (h0 : p ∅) (step : ∀ a s, a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)) : p s := by
  induction' s using Finset.strongInductionOn with s ihs
  rcases (s.image f).eq_empty_or_nonempty with (hne | hne)
  · simp only [image_eq_empty] at hne
    simp only [hne, h0]
  · have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
    simp only [mem_image, exists_prop] at H
    rcases H with ⟨a, has, hfa⟩
    rw [← insert_erase has]
    refine step _ _ (not_mem_erase a s) (fun x hx => ?_) (ihs _ <| erase_ssubset has)
    rw [hfa]
    exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)

Induction Principle for Finite Sets via Maximum Function Values

Informal description

Let $\alpha$ be a linearly ordered type and $\iota$ a type with decidable equality. Given a function $f : \iota \to \alpha$ and a predicate $p$ on finite subsets of $\iota$, to prove that $p$ holds for any finite set $s \subseteq \iota$, it suffices to show: 1. $p$ holds for the empty set ($p(\emptyset)$), 2. For any element $a \notin s$ and any finite set $s$, if $f(x) \leq f(a)$ for all $x \in s$ and $p(s)$ holds, then $p(s \cup \{a\})$ also holds.

Finset.induction_on_min_value theorem

 [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι) (h0 : p ∅)
  (step : ∀ a s, a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (insert a s)) : p s

Full source

/-- Induction principle for `Finset`s 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)`. -/
@[elab_as_elim]
theorem induction_on_min_value [DecidableEq ι] (f : ι → α) {p : Finset ι → Prop} (s : Finset ι)
    (h0 : p ∅) (step : ∀ a s, a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (insert a s)) : p s :=
  @induction_on_max_value αᵒᵈ ι _ _ _ _ s h0 step

Induction Principle for Finite Sets via Minimum Function Values

Informal description

Let $\alpha$ be a linearly ordered type and $\iota$ a type with decidable equality. Given a function $f : \iota \to \alpha$ and a predicate $p$ on finite subsets of $\iota$, to prove that $p$ holds for any finite set $s \subseteq \iota$, it suffices to show: 1. $p$ holds for the empty set ($p(\emptyset)$), 2. For any element $a \notin s$ and any finite set $s$, if $f(a) \leq f(x)$ for all $x \in s$ and $p(s)$ holds, then $p(s \cup \{a\})$ also holds.

Finset.exists_max_image theorem

(s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Full source

theorem exists_max_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
    ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x := by
  obtain ⟨y, hy⟩ := max_of_nonempty (h.image f)
  rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩
  exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩

Existence of Maximum Image for Nonempty Finite Sets

Informal description

For any nonempty finite set $s$ in a type $\beta$ and any function $f : \beta \to \alpha$ where $\alpha$ is linearly ordered, there exists an element $x \in s$ such that for all $x' \in s$, the image $f(x')$ is less than or equal to $f(x)$. In other words, $f$ attains its maximum value on $s$ at some point $x \in s$.

Finset.exists_min_image theorem

(s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x'

Full source

theorem exists_min_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
    ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x' :=
  @exists_max_image αᵒᵈ β _ s f h

Existence of Minimum Image for Nonempty Finite Sets

Informal description

For any nonempty finite set $s$ in a type $\beta$ and any function $f : \beta \to \alpha$ where $\alpha$ is linearly ordered, there exists an element $x \in s$ such that for all $x' \in s$, the image $f(x)$ is less than or equal to $f(x')$. In other words, $f$ attains its minimum value on $s$ at some point $x \in s$.

Finset.isGLB_iff_isLeast theorem

[LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsGLB (s : Set α) i ↔ IsLeast (↑s) i

Full source

theorem isGLB_iff_isLeast [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
    IsGLBIsGLB (s : Set α) i ↔ IsLeast (↑s) i := by
  refine ⟨fun his => ?_, IsLeast.isGLB⟩
  suffices i = min' s hs by
    rw [this]
    exact isLeast_min' s hs
  rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his
  exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))

Greatest Lower Bound Characterization for Finite Sets: $\text{IsGLB}(s, i) \leftrightarrow \text{IsLeast}(s, i)$

Informal description

Let $\alpha$ be a linearly ordered type, $s$ a nonempty finite subset of $\alpha$, and $i$ an element of $\alpha$. Then $i$ is the greatest lower bound of $s$ if and only if $i$ is the least element of $s$.

Finset.isLUB_iff_isGreatest theorem

[LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsLUB (s : Set α) i ↔ IsGreatest (↑s) i

Full source

theorem isLUB_iff_isGreatest [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
    IsLUBIsLUB (s : Set α) i ↔ IsGreatest (↑s) i :=
  @isGLB_iff_isLeast αᵒᵈ _ i s hs

Least Upper Bound Characterization for Finite Sets: $\text{IsLUB}(s, i) \leftrightarrow \text{IsGreatest}(s, i)$

Informal description

Let $\alpha$ be a linearly ordered type, $s$ a nonempty finite subset of $\alpha$, and $i$ an element of $\alpha$. Then $i$ is the least upper bound of $s$ if and only if $i$ is the greatest element of $s$.

Finset.isGLB_mem theorem

[LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s : Set α) i) (hs : s.Nonempty) : i ∈ s

Full source

theorem isGLB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s : Set α) i)
    (hs : s.Nonempty) : i ∈ s := by
  rw [← mem_coe]
  exact ((isGLB_iff_isLeast i s hs).mp his).1

Greatest Lower Bound of Finite Set is a Member

Informal description

Let $\alpha$ be a linearly ordered type, $s$ a nonempty finite subset of $\alpha$, and $i$ an element of $\alpha$. If $i$ is the greatest lower bound of $s$, then $i$ belongs to $s$.

Finset.isLUB_mem theorem

[LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s : Set α) i) (hs : s.Nonempty) : i ∈ s

Full source

theorem isLUB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s : Set α) i)
    (hs : s.Nonempty) : i ∈ s :=
  @isGLB_mem αᵒᵈ _ i s his hs

Least Upper Bound of Finite Set is a Member

Informal description

Let $\alpha$ be a linearly ordered type, $s$ a nonempty finite subset of $\alpha$, and $i$ an element of $\alpha$. If $i$ is the least upper bound of $s$, then $i$ belongs to $s$.

Multiset.exists_max_image theorem

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

Full source

theorem Multiset.exists_max_image {α R : Type*} [LinearOrder R] (f : α → R) {s : Multiset α}
    (hs : s ≠ 0) : ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y := by
  classical
  obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)
  exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩

Existence of Maximum Image for Nonempty Multisets

Informal description

For any linearly ordered type $R$ and any function $f : \alpha \to R$, if $s$ is a nonempty multiset of elements of type $\alpha$, then there exists an element $y \in s$ such that for all $z \in s$, $f(z) \leq f(y)$.

Multiset.exists_min_image theorem

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

Full source

theorem Multiset.exists_min_image {α R : Type*} [LinearOrder R] (f : α → R) {s : Multiset α}
    (hs : s ≠ 0) : ∃ y ∈ s, ∀ z ∈ s, f y ≤ f z :=
  @exists_max_image α Rᵒᵈ _ f s hs

Existence of Minimum Image for Nonempty Multisets

Informal description

For any linearly ordered type $R$ and any function $f : \alpha \to R$, if $s$ is a nonempty multiset of elements of type $\alpha$, then there exists an element $y \in s$ such that for all $z \in s$, $f(y) \leq f(z)$.