ciInf_eq_bot_of_bot_mem — Mathlib

English

Let α be a conditionally complete linear order with a bottom element ⊥. For any index set ι and any function f : ι → α, if ⊥ occurs among the values of f, then the infimum of f is ⊥.

Русский

Пусть α — частично упорядоченный линейный порядок с нижним пределом ⊥. Для множества индексов ι и функции f : ι → α, если значение ⊥ встречается в множестве значений f, то инфимум последовательности f равен ⊥.

LaTeX

$$$ \bot \in \mathrm{range}(f) \Rightarrow \inf_{i \in ι} f(i) = \bot $$$

Lean4

theorem ciInf_eq_bot_of_bot_mem [OrderBot α] {f : ι → α} (hs : ⊥ ∈ range f) : iInf f = ⊥ :=
  csInf_eq_bot_of_bot_mem hs

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