Mathlib.Data.Fintype.Lattice

Finset.sup_univ_eq_iSup theorem

[CompleteLattice β] (f : α → β) : Finset.univ.sup f = iSup f

Full source

/-- A special case of `Finset.sup_eq_iSup` that omits the useless `x ∈ univ` binder. -/
theorem sup_univ_eq_iSup [CompleteLattice β] (f : α → β) : Finset.univ.sup f = iSup f :=
  (sup_eq_iSup _ f).trans <| congr_arg _ <| funext fun _ => iSup_pos (mem_univ _)

Finite supremum equals indexed supremum: $\sup_{x \in \alpha} f(x) = \bigsqcup_{x \in \alpha} f(x)$

Informal description

For any function $f : \alpha \to \beta$ where $\beta$ is a complete lattice, the supremum of $f$ over all elements of a finite type $\alpha$ (obtained via `Finset.univ.sup f`) is equal to the indexed supremum $\bigsqcup_{x \in \alpha} f(x)$.

Finset.inf_univ_eq_iInf theorem

[CompleteLattice β] (f : α → β) : Finset.univ.inf f = iInf f

Full source

/-- A special case of `Finset.inf_eq_iInf` that omits the useless `x ∈ univ` binder. -/
theorem inf_univ_eq_iInf [CompleteLattice β] (f : α → β) : Finset.univ.inf f = iInf f :=
  @sup_univ_eq_iSup _ βᵒᵈ _ _ (f : α → βᵒᵈ)

Finite infimum equals indexed infimum: $\inf_{x \in \alpha} f(x) = \bigsqcap_{x \in \alpha} f(x)$

Informal description

For any function $f \colon \alpha \to \beta$ where $\beta$ is a complete lattice and $\alpha$ is a finite type, the infimum of $f$ over all elements of $\alpha$ (computed via `Finset.univ.inf f`) is equal to the indexed infimum $\bigsqcap_{x \in \alpha} f(x)$.

Finset.fold_inf_univ theorem

[SemilatticeInf α] [OrderBot α] (a : α) : (Finset.univ.fold min a fun x => x) = ⊥

Full source

@[simp]
theorem fold_inf_univ [SemilatticeInf α] [OrderBot α] (a : α) :
    (Finset.univ.fold min a fun x => x) = ⊥ :=
  eq_bot_iff.2 <|
    ((Finset.fold_op_rel_iff_and <| @le_inf_iff α _).1 le_rfl).2 ⊥ <| Finset.mem_univ _

Infimum of Universal Set in Finite Meet-Semilattice is Bottom Element

Informal description

Let $\alpha$ be a meet-semilattice with a least element $\bot$. For any element $a \in \alpha$, the infimum of all elements in $\alpha$ (computed via folding the minimum operation over the finite universal set) equals $\bot$. In other words, $\text{fold min } a \text{ over } \alpha = \bot$.

Finset.fold_sup_univ theorem

[SemilatticeSup α] [OrderTop α] (a : α) : (Finset.univ.fold max a fun x => x) = ⊤

Full source

@[simp]
theorem fold_sup_univ [SemilatticeSup α] [OrderTop α] (a : α) :
    (Finset.univ.fold max a fun x => x) = ⊤ :=
  @fold_inf_univ αᵒᵈ _ _ _ _

Supremum of Universal Set in Finite Join-Semilattice is Top Element

Informal description

Let $\alpha$ be a join-semilattice with a greatest element $\top$. For any element $a \in \alpha$, the supremum of all elements in $\alpha$ (computed via folding the maximum operation over the finite universal set) equals $\top$. In other words, $\text{fold max } a \text{ over } \alpha = \top$.

Finset.mem_inf theorem

[DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} : a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i

Full source

lemma mem_inf [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} :
    a ∈ s.inf fa ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i := by induction' s using Finset.cons_induction <;> simp [*]

Membership in Infimum of Finite Family of Sets

Informal description

Let $\alpha$ and $\iota$ be types with $\alpha$ having decidable equality, and let $s$ be a finite set of elements of type $\iota$. For a function $f \colon \iota \to \text{Finset } \alpha$ and an element $a \in \alpha$, the element $a$ belongs to the infimum of the sets $f(i)$ over $i \in s$ if and only if $a$ belongs to $f(i)$ for every $i \in s$. In symbols: \[ a \in \bigwedge_{i \in s} f(i) \leftrightarrow \forall i \in s, a \in f(i). \]

Finite.exists_max theorem

[Finite α] [Nonempty α] [LinearOrder β] (f : α → β) : ∃ x₀ : α, ∀ x, f x ≤ f x₀

Full source

theorem Finite.exists_max [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) :
    ∃ x₀ : α, ∀ x, f x ≤ f x₀ := by
  cases nonempty_fintype α
  simpa using exists_max_image univ f univ_nonempty

Existence of Maximum in Finite Domains

Informal description

Let $\alpha$ be a finite nonempty type and $\beta$ a linearly ordered type. For any function $f \colon \alpha \to \beta$, there exists an element $x_0 \in \alpha$ such that for all $x \in \alpha$, $f(x) \leq f(x_0)$.

Finite.exists_min theorem

[Finite α] [Nonempty α] [LinearOrder β] (f : α → β) : ∃ x₀ : α, ∀ x, f x₀ ≤ f x

Full source

theorem Finite.exists_min [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) :
    ∃ x₀ : α, ∀ x, f x₀ ≤ f x := by
  cases nonempty_fintype α
  simpa using exists_min_image univ f univ_nonempty

Existence of Minimum for Finite Functions on Linear Orders

Informal description

Let $\alpha$ be a finite nonempty type and $\beta$ be a linearly ordered type. For any function $f \colon \alpha \to \beta$, there exists an element $x_0 \in \alpha$ such that for all $x \in \alpha$, $f(x_0) \leq f(x)$.