ciInf_mem — Mathlib

English

Let α be a conditionally complete linear order with WellFoundedLT. For any nonempty index set ι and any f : ι → α, iInf f ∈ range f.

Русский

Пусть α — условно полноупорядоченный линейный порядок с хорошим основанием LT. Для любого непустого множества индексов ι и функции f : ι → α инфимум последовательности достигается: iInf f = f(i) для some i.

LaTeX

$$$ \exists i \in ι, f(i) = \inf_{j} f(j) $$$

Lean4

theorem ciInf_mem [Nonempty ι] (f : ι → α) : iInf f ∈ range f :=
  csInf_mem (range_nonempty f)

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