exists_minimalFor — Mathlib

English

If (f''s) is finite and s ≠ ∅, then there exists i ∈ ι such that f i ∈ s and f i is minimal among {f j | j ∈ s}. This is the dual version of the maximal-for statement with respect to the order on α.

Русский

Если (f''s) конечно и s непусто, то существует i ∈ ι такой, что f i ∈ s и f i минимален среди {f j | j ∈ s}. Это двойственная версия по отношению к максимуму.

LaTeX

$$$\exists i \in \iota,\ f(i) \in s \wedge \forall j \in \iota,\ f(j) \in s \rightarrow f(i) \le f(j).$$$

Lean4

theorem exists_minimalFor (f : ι → α) (s : Set ι) (h : s.Finite) (hs : s.Nonempty) : ∃ i, MinimalFor (· ∈ s) f i :=
  Finite.exists_maximalFor (α := αᵒᵈ) f s h hs

Похожие утверждения